Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people.
It depends on the execution order. Model computations can be scheduled differently depending on what else is going on. You need extra effort to guarantee the same order of execution. For example if addition saturates at 8, then 4+5-2 is non-associative.
I think people sometimes overestimate what proving something means. For example the 4 color problem was a computer assisted proof from a long time ago. I doubt that many people actually read the proof even though leafing through the book is kind of fun if you can find a copy. Another example is the Kepler conjecture on sphere packing. The peer reviewers said they couldn't vouche for its correctness. While reviewers are volunteers with busy schedules, a lack of interest surely was part of the issue. This motivated Hales to formaly check his own proof (Gonthier formalized the four color problem earlier). But you can be sure that no one had been waiting for the Kepler conjecture to be proved in order to pack their spheres. Otoh, at the opposite extreme, the proof of FLT greatly advanced the field because the modularity theorem behind Wiles' proof is at the heart of a great section of math theory.
Yep. And the model is practically unbounded in its knowledge of math. So people should keep that in mind when they read anything about its level of intelligence.
I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.
Right and these are perfect math objects: a perfect sphere has only one parameter. You can't describe a real life ball in Lean. You may be able to describe a class of real life balls using probability theory.
Yes for a fixed amount of effort the more you dedicate to formalization the less room there is for exploration. So the constraint is the total budget. The other constraint is if your language doesn't have the concept of gravity it is less likely you are developing the theory of gravity. So if you want to talk about modularity lifting in Lean you need to build up theories on elliptic curves, modular forms, modular curves etc first, because the library doesn't have them even if you consider them elementary. So now if you have a Lean proof with little effort I can infer that it is unlikely to say anything deep about these subjects. If you only have a paper proof, otoh, that doesn't bound your distance from the basics for me.
Having a Lean proof is an assurance that you proved something. But without going through the definitions we can't know what you proved. This part can't be mechanized. It's like a program that is compiled will likely run, but you can't say it will produce what you want. FLT stands out as everyone can read the statement. This is not true for most open math problems.
For example mathlib doesn't develop basic theories like Riemann surfaces, and doesn't have Riemann existence theorem etc. So if you develop a complex analysis result without these there are many things you can't even talk about. Developing basic theories takes time and efforts. See Anthropic FLT proof for example. While 13 million lines headline count may contain 50% redundancies due to agent swarming, on the net they still dedicated millions lines of effort to develop basic theories. And often they developed specialized versions in concrete theories just sufficient for their needs. For example they still don't have Riemann surfaces nor Riemann existence.
Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak. Despite the community efforts, the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved. And formalization steps are small and labor intensive, so you are often constrained in how far you can go by the volume of code you produce. It's also telling that Lean tooling isn't advanced by the labs despite the resources they put into their effort, the importance they attache to Lean and the frictions they must have run into constantly. The release feels more like a retreat by the labs.
Fun challenge: find the formal definition of simple_closed_curve in the essay and tell me if you believe you learned anything about a planar curve.
BTW the essay is eminently readable for anyone interested in math. Hales wrote it in favor of formalized math and to educate his peers and students about it.
If you actually looked into how agents proved FLT you would be even more amazed by the fellow human beings who are able to keep all this in their heads! I for one can only begin to grasp the scope with AI and scripts.
AI is very helpful with understanding AI proofs. Agent swarms produce messy proofs overall but locally they are excellent and can teach anyone who wants to study them. No one controls math (in a material way funders do control an aspect of practicing math). Still, theorems are already true before we prove them. The difference a proof makes is whether it convinces the reader.
He spent years formalizing his sphere packing theorem because the proof (human produced) was already beyond the ability of peer reviews. Now his formalization effort likely can be easily reproduced by a model. However one should read his experience about what a formal proof is: often the problem is the statement not the proof. The example he gave is the Jordan curve theorem. It's actually quite challenging to formalize the concept of a planar curve (there are space filling curves). So it is not necessary that someone can look at a formal statement and say aha it is about a planar curve, unlike FLT where there is not much problem in recognizing what the statement is about.
This doesn't contradict what I said. But I do appreciate the fact AI can produce side effects not just humans. I made it sound like only human knowledges matter. That's too narrow.
I didn't say that. I am responding to "In a way this is probably 50-100 years of math progress by humans." I am actually very excited about AI proof and I am working overtime in my own way to try to comprehend as much as I can.
Another way to state this: math theorems are like programs without side effects; it is immaterial whether a program without side effects is ever run. We study math for the side effects: it changes how we organize our thoughts.
Math is the tool humans use to compress knowledge. So until we can comprehend it there really isn't much progress. Math theorems are tautologies, the truth of which are not dependent on proofs and proofs are erasable, at least classically. But the AI progress is exciting and AI proofs are a gold mine for humans (at least non domain experts) to explore.
Light slows down in dielectric materials because as an em wave it interacts with the polarization of molecules. Neutrino has very little interaction with matter, OTOH.
LLMs like even the sota flash models have great range of background math knowledge and have no problem reading and understanding flt level of math. On the other hand you don't want to go through 13 million lines of often repetitive code line by line. Models are great at synthesizing math content out of code. My contribution is to steer it through subjects of most interests to me, drill down into jargons that can be confusing, be creative in using computation for illustration (which coding agents can execute very proficiently) etc.
I enjoy learning math from LLM proofs with the help of LLMs https://github.com/htzh/flt_for_human . It is amazing how well models do when they are well grounded by formalized proof traces (even if created by other models).
Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.
I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.