Classification of Finite Simple Groups Formalized in Lean
j / k
|
Down or up a comment |
h / l
|
Previous or next link |
?
|
This help |
Maybe my understanding of Lean is wrong; I'm thinking of it as a programming language but for Math.
One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.
What they’re not that great at is the type of improvements that really make a big difference: big simplifications etc. This is not super suprising when you understand how this works.
Firstly proofs in lean (and I think many other assistants) are essentially functions which take hypotheses and instantiate a particular type. That type being equivalent (due to the Curry-Howard correspondence) to a proof of some proposition. The assistant uses dependent type theory to make sure all the types match up at each step, which is what makes it rigorous. So the task of simplifying a proof is basically finding a route through an infinite-dimensional space where you know your starting location and the desired end point, but at any step you can go in basically any direction you like so long as you can justify your step. You justify a step by either choosing from a (vast at this point) library of lemmas and theorems that are in your standard library, or by recursively building the proof/function you need to justify the step you want to take using this same process you’re trying to use for simplification. This is incredibly flexible, but means you’re actually spoiled for choice and planning is hard.
Secondly, in “pen and paper” proofs, LLMs don’t know the difference between steps which are important/easy/hard/intuitive/non-intuitive for human mathematicians, so lots of the proofs they produce are extremely clunky and pedantic in places and dwell for ages over details that are obvious and would usually be skipped over and then will move very fast through things that justify more attention. This unevenness is part of what makes their proofs hard for humans to work through, but also means they are generally poor judges of what would actually constitute a decent simplification.
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
Some books assume 0 is Natural but other start from 1.
In some books all Rings https://en.wikipedia.org/wiki/Ring_(mathematics) have a multiplicative identity. Almost all books assume Algebras have an identity, but there may be weird cases.
Some books say in the first page that they will assume all groups are Abelian/Commutative, and not repeat the assumption in each page.
There are like 8 conventions to define the Fourier Transform. All are equivalent, but each one add different constants here and there. Beware to combine formulas from different books.
I guess it's easier for the computer to track the details and remember to translate the names in each book article to a consistent set of definitions.
Probably this will be done in some form in the coming months.
Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.
One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.
Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).
LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.
The original proof was a collaboration of ~100 mathematicians, if Tao is correct then we should expect to see more such collaborations in the future like we do in e.g. physics.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.
Lean's type theory kinda gives up on that idea: Mathlib gleefully postulates impredicative propositions with the axiom of choice, quotient types, etc. All in all, I'd say that Lean is much closer in spirit to De Bruijn's AUTOMATH project (which pre-dates Martin-Löf!), whose goal was to formalise classical math textbooks using dependent types.
>However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem.
[1]https://axiommath.ai/research/the-enormous-theorem-formalize...
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.
In this case the statement is unusually complicated but still much much easier to verify than the proof itself.
Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.
Humans have to establish trust in this.
After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it
The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.
It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.
Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.
https://en.wikipedia.org/wiki/Monster_group
No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.
Like, proving that in the absence of hardware faults, some optimizer for JavaScript can never result in arbitrary memory accesses.
Or that some database doesn't violate data semantics under ANY condition.
Or that as long as not too many sensors fail, a plane autopilot will not go and do anything that would lead the plane to exceed safe speeds and forces/accelerations. (Won't just go crash the plane or drop it from the sky in one or more pieces just because some few sensors froze or caught lightning or something.)