fspeech

Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean would ensure that the translation is correct.

Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.

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.