I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.
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.
Uhm three ideas about that (they don't solve the problem on their own, they just show mathematicians care about this issue)
Category theory can be viewed as a framework to make math more modular and compatible. For example topos theory can be used to transport definitions to other "mathematical universes" of sorts
Another point of view is that is working with synthetic mathematics which is a bit like "programming" mathematics with an abstract API. The opposite, analytic mathematics, leak implementation details (for example, the von Neumann construction of natural numbers, which is analytic, leak the implementation detail that 0 is defined as the empty set; but the peano axioms are synthetic and doesn't leak any such details)
There is also the principle that two mathematical objects that are isomorphic (have the same structure) are actually the same thing. For example if you construct the natural numbers two different ways, they are "the same thing" in a sense. This usually is stated informally, but a rigorous formulation of that is the univalent principle
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.
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.
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.
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.
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.
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.
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.
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.
reply