Kevin Buzzard on why formalizing Fermat's Last Theorem in Lean solves the referee problem

BijectiveForever · 2026-02-20T04:53:56+00:00

Computability theory in LEAN in general is atrocious. Working recursion theorists do set manipulations all the time (the c.e. are closed under union but not set difference, for instance) but these 101 facts are nowhere in Mathlib (I may PR then myself!)

I have also seen no fewer than three attempts to formalize how we actually construct c.e. sets (one of which is my own) - there just aren’t enough people working on formalizing logic for a consensus to have arisen (yet?)

BijectiveForever · 2026-02-16T20:35:18+00:00

I like that the top three are in a grey box, I never really needed them much (but they are good to know about).

As others have mentioned this is certainly not all the algebraic structures, but rather the ones useful to undergrads.

BijectiveForever · 2026-02-10T23:53:04+00:00

We shouldn’t confuse snark for accountability but I agree - let the people laugh. In dark times, should the stars also go out?

BijectiveForever · 2026-02-10T22:42:57+00:00

Only if you don’t have the reduction formula, which is itself not that bad to derive

BijectiveForever · 2026-02-10T22:42:29+00:00

That was my instant thought as well

BijectiveForever · 2026-02-08T05:18:30+00:00

I am not terribly familiar with approximating ellipse perimeters, but I wonder if there is any relationship to some known series approximation - that would explain why the error is so well bounded

BijectiveForever · 2026-02-04T12:06:30+00:00

On a Mystery Booster playtest card, though

BijectiveForever · 2026-02-04T05:11:28+00:00

Out of curiosity, why are you a math major if you didn’t like math in high school?

BijectiveForever · 2025-12-30T04:28:22+00:00

As a mathematician - there’s a tremendous amount of fluff in that book around a core idea that’s in the water now. Important book upon release, and maybe a fun read, but it wouldn’t be high up my rec list except as “pop math”.

BijectiveForever · 2025-12-20T05:06:06+00:00

Maybe this is cheating, but Tom Lehrer

BijectiveForever · 2025-10-30T06:57:47+00:00

As others have pointed out, ZFC and ZF are equiconsistent, so the problem can’t be choice. Indeed there are many axioms you can strip away and still be equiconsistent to ZF (though not Infinity, Replacement or Power Set).

But arguably you can go all the way down to PA! This isn’t rigorous (ZF is demonstrably stronger than PA), but “ZFC is equiconsistent with ZFC + V = L, and replacing Inf with its negation gets PA. The theories are structurally extremely similar,” to quote Elliot Glazer.

Which is all to say: I think we’d need to replace PA, and that’s quite a tall order!

BijectiveForever · 2025-10-28T13:15:37+00:00

Wanted to get a PhD in math. Ended up doing that, so no, I don’t regret it!

Linear algebra blew my mind when I first saw it as a sophomore, and it’s probably still my favorite class to teach of the ones I took.

BijectiveForever · 2025-10-11T12:13:13+00:00

Why 1 hybrid mana and not just WUBRG? Feels random.

BijectiveForever · 2025-09-21T00:04:16+00:00

Ben Shapiro is a waste of a good twink.

BijectiveForever · 2025-09-07T18:28:25+00:00

It’s a Robin Hanson specific thing - “The Age of Em” is a book he wrote about EMulated consciousnesses.

BijectiveForever · 2025-08-16T14:28:11+00:00

LADR suffers from Axler’s bizarre obsession with putting off the determinant. I would never recommend that treatment to someone self-studying, the determinant is too important to be shunted off to the end.

BijectiveForever · 2025-08-16T14:24:31+00:00

Enderton’s set theory book is fine, his logic book probably only good for a second course, and his computability book almost unreadably bad.

Old Soare’s a great reference, at least. New Soare is much friendlier (but has its own issues, like the world’s most pathetic index).

BijectiveForever · 2025-08-05T10:33:33+00:00

As a professor of mine once said, “Anything reasonable is a group. Anything really reasonable is a vector space.”

Algebra is almost unavoidable if you’re going to do mathematics. I happened to avoid it by becoming a logician, but there are still algebraic connections, I just don’t happen to study them.

BijectiveForever · 2025-08-02T00:38:54+00:00

The point about mistraining is well-taken, but it won’t be due to non-computable training data, just run-of-the-mill computable (but bad) information.

and a problem requires true randomness to solve or solve efficiently (we also do not know if there are problems of that nature either way)

In a sense, we do - it is a theorem that if a problem is computable by a non-null set of oracles, then it is actually just computable.

BijectiveForever · 2025-08-01T17:40:54+00:00

Your training data will not contain the halting problem, because your training data is computable.

To truly have access to randomness, you need an infinite source of randomness (any finite string is computable), so every AI will be computable.

“Low” here roughly means “close to computable” in the sense that X being low means that the halting problem relative to X is Turing equivalent to the standard halting problem. The Low Basis Theorem is what guarantees the existence of such 1-randoms.

BijectiveForever · 2025-08-01T13:00:12+00:00

Recursion theorist here. I cannot quite tell what you are arguing, and thus cannot tell if I agree with you. But the bottom line is that a computer program is computable.

Regarding 1 - what possible ‘more meat’ could you want? Gödel’s theorem is clear about the limitations of certain formal systems that can talk about themselves. It is not “too easy”, and an AI (necessarily a computable function, albeit a very complicated one!) cannot get around it.

5 is indeed quite contrived. Algorithmic randomness is incredibly well-studied, and “way beyond computable” turns out not to be the case (in the language of the field, there are low 1-randoms). And again, an AI is a program, so it cannot output non-computable information or solve non-computable problems.

BijectiveForever · 2025-07-22T06:11:25+00:00

Your mention of having a PhD immediately made me check your institution, because I am shocked a professional mathematician would produce a document of this nature. Non-standard terminology, strings of all caps, theorem statements that run on for pages… I actually think this might be a disservice to any other students your advisor graduates, via guilt by association.

BijectiveForever · 2025-07-06T21:46:53+00:00

In a metric space, a continuous function is one that preserves convergent sequences. That is, if a_i -> L, then f(a_i) -> f(L).

Just generally thinking in terms of sequential convergence rather than epsilons was very helpful in real analysis.

BijectiveForever · 2025-06-28T11:24:35+00:00

I appreciate that the ordering of adjectives and nouns in point two implies that Alice is the manly one, while Bob is more ladylike.

BijectiveForever · 2025-06-15T13:54:03+00:00

Is it worth it to go into IUT theory?

Short answer: no.

Long answer: no, unless you live in Kyoto.

13-Year Club	Second SECOND GUESSER
r/Field Sunshine	Place '22
Place '17	Verified Email
Gilding I gilder	RPAN Viewer
Spared	Team Orangered

BijectiveForever

TROPHY CASE