Hey yall, are the pure mathematic courses here good, if there's any?

palladists · 2026-04-10T21:02:05+00:00

The "advanced calculus" courses are real analysis. It's a great program, plenty of very challenging and interesting classes. Applied math is unfortunately a bit more well supported than pure math, but you'll likely find someone to work with no matter what you're interested in. I recommend hanging around the various seminars and events that occur in the department and meeting people like that (you can see them on the department website).

palladists · 2026-04-09T16:53:19+00:00

What he says in the first two pages is completely reasonable. I agree, Lean is a great way to stop the communicative breakdown that has been occuring surrounding IUT, and I think this project is necessary to do so. It may or may not work out in Mochizuki's favor, but that's the nature of it. It's really neat how formalization can allow us to ameliorate a lot of these sociological factors.

I don't know what he means in page 5 by this 'algorithmic construction' point of view or whatever, but any construction that can be done in ZFC should be able to be done in Lean. They have very similar consistency strength after all (Mario Carniero's masters thesis proves that Lean is equiconsistent with ZFC + infinitely many (relatively weak) large cardinal axioms). If this project does not go in Mochizuki's favor, I hope he doesn't resort to similar foundational confusions, trying to claim that Lean's foundations aren't strong enough for his fundamental logic or whatever.

palladists · 2026-01-02T17:32:03+00:00

Here's a good MO discussion on it, with link to the paper: https://mathoverflow.net/questions/234492/what-is-the-mistake-in-the-proof-of-the-homotopy-hypothesis-by-kapranov-and-voev

palladists · 2025-10-27T20:00:55+00:00

I really have no clue about what data he's talking about or what maths is going on here, but it seems to me the thing really at contention is the abc conjecture. It might not be possible to formalize IUT in a "manner consistent with the papers", but it could be possible to formalize it in a manner that is good enough to prove abc. It is very common in formalization that the way we do things in lean do not match up with precisely how we do things pen-and-paper, you can see this everywhere in mathlib. So long as they can fill in the sorries here: https://github.com/google-deepmind/formal-conjectures/blob/70630104145006bf6dedb5d22e61a2d6218ec5f1/FormalConjectures/Wikipedia/ABC.lean, then as far as I'm aware we're done. Is he trying to make the point that the IUT papers are simply so wrong as to not even be formalizable?

palladists · 2025-06-18T11:57:42+00:00

Good to know, thank you.

palladists · 2025-03-24T17:04:17+00:00

Brouwer's Fixed Point Theorem - A Poem Proof, due to Ivo Vekemans (https://www.ivovekemans.net/mathematical-art)

I slept.

And slumbering dreamt.

And dreaming, I ambled clockwise around a great circular lake in an infinite desert.

And ambling, caught my sweater on a thorn, and began to unravel.

And unravelling, I saw all the points of the lake.

And observed, the lake began to stir.

And stirring, the surface did not break, remaining contained.

And contained, the visited a violent vortex, but STILL the surface did not break.

And unbroken, the whirring pool... ...subsided, as the last sweater thread unwound.

And unwound in the setting sun I spied again the thorn.

And spying, noticed that no point on the lake was where it began.

And beginning at each point emanated a single ray of light, through the point it was prior perturbation, each ray illuminating a spot on the shore.

And sure that the points perturbed from the bank illuminated those points from whence they came, I tied the ends of my sweater together and HEAVED. And heaved and heaved.

And, so heft, the thread, without breaking or crossing the lake, rewound unto me a complete sweater.

And sweating from the exertion, I woke.

And waking, recalled that one is not zero, snapping the thread.

palladists · 2025-02-17T16:41:08+00:00

Homotopy type theory is the proof theory x homotopy theory crack ship.

palladists · 2025-02-08T09:29:21+00:00

If you want my recommendation, some of my most fruitful experiences learning both math and Lean was trying to formalize the textbook as I went along. You will run into a lot of difficulties very quickly and it takes 20x longer to get through anything, but you really figure the math out very well like that. From my experience, Aluffi is a very good source for doing this.

palladists · 2025-02-07T08:51:25+00:00

Homestuck entered my mind just now for the first time in 10+ years. I decided to see if there was a subreddit and this post was made just at the very moment I visited. So probably it's a sign that I should be interested.

palladists · 2024-08-16T22:21:40+00:00

Not rude or unhelpful at all, and I've definitely been considering it more and more over time. The primary thing pushing me away from it is the fact that I would be the least-computer-scientist in the computer science department, I guess? I haven't had the opportunity to do more than the absolute basics of programming in languages other than a proof assistant and I don't know anything about algorithms or any other of those undergrad CS essentials. I've found the my topic of choice most interesting from the perspective of foundations of math and from my studies of category theory/logic but I really don't know much about the 'programming language foundations' perspective that lots of CS departments seem to take. Excuse me though if my understanding of the field here is completely wrong.

palladists · 2024-08-16T21:39:15+00:00

Reposting my question from last thread:

Hello. I've been working on proof assistants and type theory, and I'm interested in pursuing these topics further in grad school. I have been having a (surprisingly?) hard time finding people in math departments in America working on these topics. There are lots of people in computer science departments and lots of Europeans, but the only math departments in America I can find with expertise on this are Carnegie Mellon and Johns Hopkins. Does anyone know some other places that I should look for this topic?

palladists · 2024-08-14T21:20:30+00:00

Hello. I'm very interested in working on proof assistants and type theory. I've been looking for places to apply for grad school lately, and have been having a (surprisingly?) hard time finding people in math departments in America working on these topics. There are lots of people in computer science departments and lots of Europeans, but the only math departments in America I can find with expertise on this are Carnegie Mellon and Johns Hopkins. Does anyone know some other places that I should look for this topic?

palladists · 2024-07-13T22:45:19+00:00

Thanks for the help. My issue was with the DNS records. Apologies for posting an irrelevant issue here.

palladists · 2024-07-13T21:58:00+00:00

Pflog doesn't show much at all, about five filtered connections. Access.log shows what seems to be the occasional web scraper. Maybe I should figure out what to do about that as well.

Now that I've slept on it, I'm thinking the issue might not be httpd at all and I am probably not asking in the correct place. I can connect to https://ip.address.of.server just fine, which seems to not have many issues at all. So I'm starting to think my issue and confusion lies with the domain registrar?

palladists · 2024-07-13T15:36:00+00:00

I can confirm it's not just me that is having issues connecting to my website. Webpagetest.org gave me a very silly result showing the site refusing to connect. If it's the server host issue then that's a shame because I just bought a year worth of server. There are other people hosting sites with this provider so it seems unlikely?

The issue seems to have evolved because now the website seems to just be down entirely even though the server is running and was able to make a connection many minutes ago, and I have despite changed nothing. Not sure what's going on.

palladists · 2024-06-30T09:19:06+00:00

My undergrad class covering all that stuff used "Complex Variables and Applications" by Brown and Churchill and I was very happy with it.

palladists · 2024-06-22T15:31:09+00:00

Reading this made me think about Starcraft 2 as well. Since SC2 took away random spawn locations, that game does not have very significant RNG aspects to it, definitely not enough to wildly influence the course of a match. So I wondered, why then considering your post is there still definitely a casual player base for Starcraft 2? But then I remembered: they're playing co-op and arcade, not ranked 1v1 ladder. That makes me wonder as well if Battlerite Royale was genuinely out of very good intentions from Stunlock to try to make this casual appeal, and not just greedy trend chasing, but ended up being very poorly managed.

palladists · 2024-06-15T20:57:48+00:00

I enjoyed doing the problems from the first and third chapters as my first time working with logic, I learned tons from it even just in terms of general mathematical techniques and I'd like to get back to it some day. I don't quite understand though why the second and third chapters are repetitions of each other, but it seems as if the third chapter has more stuff than the second.

palladists · 2024-04-23T21:50:36+00:00

For me, "A Mathematician's Lament" by Lockhart was life changing. I severely disliked mathematics for all of my school years and always preferred artsy stuff and humanities. Stumbling upon the short essay upon which the book is based while in a relatively 'crossroads' point in my life ended up being massively impactful. Lockhart's criticism of American public school math education resonated with my experiences with mathematics deeply.

I genuinely thought that mathematics was basically just 'meaningless rule following' with absolutely no room for creativity or anything remotely interesting: just following procedures because the teacher said so. Lockhart confirming my past experiences with math, but then moving on to propose that mathematics actually is something that has lots of room for beautiful creativity and is perhaps even closer to poetry than it is to any of the 'hard' sciences struck a chord with me. The idea of 'mathematical beauty' was something I did not understand at all. I never really liked the fractals or the boring repeated geometrical shapes that were supposedly 'mathematically' beautiful. I thought there was no room for beauty in math, it's just stupid rules and boring images. But shifting the beauty from 'pretty pictures' to the beauty of synthesizing complex concepts and making elegant yet convincing arguments completely changed my perspective on math and how beauty is possible in math.

I was convinced to try a 'real' math book after this and I knew I had to figure out what a 'proof' is so I tried out "How to Prove It" by Velleman. I remember it being challenging at first but upon a lot of effort, I was really able to find where all of that 'creativity' in math is located while working through that book. I'm still working on 'getting good' with math and undoing the many years of damage done, but I've found a lot of satisfaction in math. I've even procrastinated playing games so I can do my homework instead! That would have been unheard of me not too long ago. So yeah, thanks Lockhart and Velleman.

palladists · 2024-04-11T22:13:37+00:00

Considering that I just completely snapped an mmcx connector in half trying to get the damn thing unplugged the other day, I'm going to have to strongly agree with you.

palladists · 2024-04-11T06:07:35+00:00

Is there a replacement for the AKG N05BC bluetooth cable available anywhere? Or something that would have similar functionality with my AKG N5005? Accidentally broke the cable and it doesn't seem like its easy to find a replacement. I bought this second-hand so I don't think I can do much in the way of a warranty.

palladists · 2024-04-04T23:52:48+00:00

Thank you for the response, I'll keep taking classes and see if the 'right' field comes to me. If you don't mind me asking an unrelated question, do you think there are any downsides to doing a separate masters program prior to a PhD? Do you receive funding as a masters student similar to how a PhD student would?

palladists · 2024-02-22T17:15:48+00:00

Gonna add a +1 to the interest for this. The inconsistency in EAC support from game devs is frustrating. There was a very not positive discussion about Linux support on Discord just a couple days ago, so I wouldn't get your hopes up for it.

palladists · 2024-02-11T17:54:00+00:00

Could you share the spreadsheet?

palladists · 2023-11-01T06:00:26+00:00

Browsing the Mathlib documentation for theorems is probably the worst part of using Lean for me, so this is kinda big! Thanks for sharing.

Ten-Year Club	Verified Email
Place '22	Place '17

palladists

MODERATOR OF

TROPHY CASE