There are some (typically small) simplifications that computers are indeed good at. These could be thought of as analogous to compiler optimizations - they’ll see that your proof is basically composing several lemmas and that some of the work in the middle can be removed so it can just do that. In many cases with lean if you post a short to medium-length proof into an llm it can suggest these types of small improvements for you.
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.
I think there are a lot of practical applications where something that works few-shot and doesn't require training is quite appealing if the cost of inference is low. That's the sweet spot for Jev and similar models. If you have time and an eval set to train it, clearly a "real" special-purpose classifier should have much better performance (and for most applications cheaper cost/faster inference), but Jev and friends are way better than using a full-fat transformer LLM for a classification task.
As an example, I've been using winnow running locally as a decision model in openchamber to select between llms for doing various tasks. I don't have an eval set of different coding and other tasks that I could use to train a proper classifier. This I just download off huggingface and it works out of the box and has cut my token spend to a fraction of what it was. So it's good enough to be beneficial.
As an aside, the professor in question is Richard Borcherds, fields medalist. He is probably most well known for proving the “Monstrous Moonshine” conjecture of Conway and Norton that there is some sort of correspondence between modular functions and representations of the Monster Group. When the conjecture was made in the 1970s, it was purely because someone noticed that a certain number was the same as the cardinality of the monster group. It seemed a crazy coincidence, so John H Conway said (playfully) that it was “Moonshine”. Hence the name “Monstrous Moonshine”.
> the professor in question is Johnny Doe, with access to 100+ unrestricted Mythos agents
Yet the folks with access to unrestricted Mythos agents tackling mathematics are hiring credentialed mathematicians. Your heuristic, applied to itself, rejects itself.
We’re a long way from that world. Does your company even interview people who don’t fit the requirements of a job position? No, of course not. So what are you filtering on, if not credentials.
This guy doesn’t just have credentials. He has record of proven results.
Because they work for a sigint agency. Secrecy is a way of life for them. They probably wouldn’t even tell their own children what they had for breakfast.
Do you honestly Jeremy Avigad (to pick one of the authors) isn't intimately familiar with the Incompleteness Theorems? For starters, Jeremy is chair in logic and philosophy of maths at CMU. https://www.andrew.cmu.edu/user/avigad/
Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?
I think the comment was poking fun at the phrase, "to formalize all of mathematics".
That makes it sound like all possible mathematics past and future in all conceivable worlds. And we already know there are undecidable or unprovable statements, higher-order logics that cannot be fully formalized, concepts about axioms themselves that cannot be axiomatized, etc.
So it cannot mean "all of mathematics", strictly speaking. Just the areas in existing mathematics that have (or can have) formal proofs.
Well since one of the authors of TFA is literally the person who was asked by the association of symbolic logic to give the memorial lecture for Goedel’s centenary the comment could scarcely have been wider of the mark.
Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”
People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...
Great link, wonderful, Formalized Formal Logic. I'll enjoy reading through it. I see, a Japanese person worked on the formalization of Gödel's Incompleteness Theorems.
『Leanを用いたGödelの第一・第二不完全性定理の形式化』
..Oh I found a newer (more complete :) version of the proofs under the same domain.
From the posted link, How to Formalize All of Mathematics, in the introduction:
> vision of how we can all work toward a world in which all, or almost all, mathematical definitions, theorems, and proofs are equipped with a formal representation
That "or almost all" feels like a wink to acknowledge the commonly misunderstood limitations of formal logic and systems. Your frustration is understandable, someone even wrote a whole book about it.
Franzén, Torkel. Gödel's Theorem: An Incomplete Guide to Its Use and Abuse
The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.
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.
reply