That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".
Most mathematicians aren't doing formalization themselves, but my impression is that a lot of them are watching with interest. I get asked "is my job secure?" quite a lot nowadays. Answer is "currently yes".
Okay, yeah my response is ultimately based on the one conversation about it that I've had with the one prof of the one math class I've taken in the last 30 years, so take that with a grain of salt.
(Tangentially, I'm so so so so angry that universities stopped offering remote classes after covid. I'd been wanting to take a bunch of classes for a long time, but it's just not feasible when you've got a full-time job in the 'burbs. I managed to get through measure theory and quantum mechanics while the window was open, and it was great. I planned to get through a few more in differential geometry and algebraic topology, but then the window closed. Feels like I'll pretty much have to wait until retirement at this point. Oh well, first-world problems.)
Edit: oh and actually, follow-up question: are these tools useful for _learning_ advanced mathematics? I looked up in Lean and its approach to topology is very non-standard, which makes me question whether I'd actually be learning math or whether I'd mainly be learning how to finagle things into Lean-friendly representations but missing the higher-level concepts.
Right now I would say that tools like Lean are not useful for learning advanced mathematics, currently you're mostly better off with pencil and paper. This might change but right now the infrastructure/tools aren't there to make experimenting with new and advanced concepts any easier than it would be on pen and paper.
Indeed. I'm not formalising FLT because I think it might be wrong -- I'm formalising it because I know the proof is correct, and using the project as an excuse to get some modern number theory into Lean's mathematics library. My hope is this will increase the chances that systems like Lean will one day be able to help modern mathematicians.
(I'm the author of the game) Unfortunately it did not. That comment was made when I was optimistic that an undergraduate who'd added more levels as a summer project would go on to PR them, but then the term started and they were distracted by their degree. We have some kind of prototypes for even/odd world (e.g. "prove odd * even is even") and prime number world (boss level: prove 2 is prime), plus a hard world consisting basically of unsolved problems such as Goldbach, Twin Prime Conjecture etc. But they never made the transition from "lean file containing a bunch of theorems" to "lots of files each containing one theorem and some rambling".
Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions:
1) Whether it will still be science fiction by 2030;
2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way.
But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions:
1) Will this still be science fiction in 2030;
2) Will ITPs be involved?
And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).
I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.
I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".
My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" foundations, and mathematicians on paper just freely (and mostly unknowingly) switch between foundations depending on what they're doing. This is problematic for a project such as formalising FLT because it involves developing mathematics in a bunch of different areas (algebra, analysis, geometry) where different foundations might be more appropriate (for example getting homological algebra working in dependent type theory has been annoying and hard for all the wrong reasons, and it's taken the Lean community years to figure out how to do it).
So I don't really understand the point made in this post. Dependent type theory makes the expression of some theorems more involved and complicated -- but set theory makes the expression of some other theorems more involved and complicated, simple type theory makes the expression of some others more involved etc etc. You're right that we're just powering through this: but formalising mathematics in Lean sometimes feels like fighting against type theory (and sometimes type theory is a very welcome foundation). The point really is that the Lean community, because of its viewpoint of "formalise all mathematics in one system", has been forced to figure out how to power through the areas where dependent type theory was not the ideal foundation. Maybe the same can be said of Mizar and set theory -- I'm unclear about how much formalisation in Mizar is motivated by "let's do this because it will be unproblematic in set theory" and how much is "let's choose to do battle with set theory". In mathlib we've decided to do everything so doing battle with dependent type theory is a necessary consequence. I find it hard to believe that another foundational choice (such as Practal) solves these sorts of problems: presumably what's actually true is that some stuff which is annoying in Lean is nice in Practal but some other stuff which is nice in Lean is annoying in Practal.
> So I don't really understand the point made in this post.
I think you understand the point perfectly well. You just don't believe that there can be a logical system better suited to a foundation of mathematics than first-order logic (set theory), simple type theory, or dependent type theory. You believe you will need to compromise, no matter which foundation you choose, so better just to pick your poison and get on with it. And I think pretty much everyone in the theorem proving space has that same opinion, so it is certainly a most reasonable opinion.
But I don't believe that the right logical foundation will make it harder to do mathematics on a computer than on paper, I think it will make it easier. In fact, I am pretty sure I have found that right logical foundation, Abstraction Logic [1]. I believe that it is indeed the best logical foundation, because it is simple and elegant (more so than any other foundation I am aware of), and it seems obvious that first-order logic, simple types, and dependent types are just special cases of it.
But a logic is not a working and proven system such as Lean + mathlib, so a lot of work needs to be done before my belief can be stated as a fact.
If you can represent algebraic geometry through mathematical objects, operations and operators, then yes.
But I don't know algebraic geometry, so I cannot say if there would be any advantage of doing it in Abstraction Logic compared to Lean. If you had any difficulties formalising algebraic geometry in Lean caused by static types (for example that there are no subtypes), then that might be where AL could help.
Also, could you do category theory in general in AL? Again, I don't know category theory well enough to say. But categories can certainly be represented as mathematical objects, so I don't see why not.
Do you have a minimal example in mind where you encountered problems in Lean?
