In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.
Metamath is interesting for education in the principles of formal proofs, because:
1. The Metamath Book is self-contained well written, simple introduction.
2. Everything is explicit, nothing is hidden.
3. Because of extremely simple syntax and semantics it's easy write own proof verifier.
The drawbacks are:
1. Non-standard approach to free and bound variables.
2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.
3. Almost no proof automation. No tactics. Long, hard to read proofs.
I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
There are other forms of logic? is intuitionistic logic as rigorous? fascinating
edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
> if it is weakened, how can you prove the same stuff?
Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.
Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.
Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).
I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on the surface to be as an outcome) human beings are different and want different things, and people are productive in different environments. In particular, people who want to formalize results within the standard framework (including zfc) are never really as a group going to care that much that lean4 doesn't let them formalize results outside of zfc.
> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
I don't know about forcing, but there's certainly a long history of emacs users trying to convince vim users that they're wrong. Without loss of generality - the same is true in the other direction of course.
Software devs are more than used to having a multitude of tools at our disposal (text editors, programming languages, Linux distros...), having strong preferences, and engaging in the delicate balancing act of advocating for our favourites while living-and-letting-live as the cosmic ballet goes on. It's part of our culture; I don't think that culture necessarily exists outside. For instance, a common layman question to ask is, "Why are there so many programming languages? Why doesn't everyone just use the same one?" And I don't think mathematicians are immune to this blind spot.
The nearest equivalent to "tooling" in math, traditionally, would be notation I suppose, and mathematicians are accustomed to eventually coalescing around a single standard notation.
Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.
My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.
This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on.
LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our complete garbage, spec and all, and say it's a proof of something.
It's not shocking at all that the people who seem to get any benefit out of LLMs in the proof assistant space are the ones who could have just don't it themselves anyway.
I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a research mathematician could actually use in real time along actual math research. The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, both individually and collaboratively (such as the recent Tau Ceti project).
Anyway, what do you mean by 'say it's a proof of something'? If you mean this in technical sense, there are plenty of examples around where single individuals or small teams have autoformalized theorems with tens or hundreds of thousands of lines Lean code that pass a comparator challenge (so the theorem is correct). If you mean this in the sense that the proof is also a proof in the eyes of humans, so that someone has actually read or understood the proof, I'm willing to acknowledge that in this area there is much work still to do. In my own experience the current LLMs are already very strong at formally proving theorems (with correct semantics), but they are still lacking in writing human-readable math prose based on these formalizations, for instance.
> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that,
Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.)
> Granted their goal was not so much speed as it was elegance,
Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit.
¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough. "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)
(Sorry for the long post, but yours brought me thinking about a bunch of different aspects.)
First of all, I did not mean to downplay elegance at all. I agree that elegance is very important and that math is very much about trying to find elegant ways to think about various problems and phenomena. It also makes math feel more human and art-like, as elegance is not completely objective. And I also agree that LLMs do not seem to currently have consistent mathematical taste. I find they often do quite ugly or unoptimal proofs, although sometimes they also surprise me with a more elegant one than what I had in mind myself. And when we pass from arguments to choosing good definitions or seeing the big picture they are often much worse. Finally, formalization efforts such as Mathlib are very interesting from the elegance point of view. I'd actually be interested to see whether it would be possible to do lecture notes or textbooks based on Mathlib, written in standard math prose so that wider crowd of mathematicians might benefit from the insights that people had while formalizing.
However, as a research mathematician, I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. These formalized versions are at least at the moment not going to have pretty proofs, and the proofs the LLM comes up with might even be different from what I'm writing in the paper (but probably in practice not very different if I'm formalizing every lemma). Still, if this can be done quickly enough, I think the result could be net positive even if the formalizations never leave my local hard drive: I will have confidence that I did not miss an edge case in the statements, where usually double-checking these things is actually a very time-consuming part of writing a paper. Thus I might be able to produce papers with less mistakes (usually non-important ones but they do happen). In this sort of workflow speed matters, and if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, and I do not mean this sarcastically!).
Returning a bit to the topic of elegance, I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition. There might also be some difference in how well this works out in practice in different fields. At least historically people in analysis (like myself) are happy to repeat known arguments in slightly different settings. It could be hard to make a version that works in every setting because different sets of assumptions could allow for a similar argument to work. Or it could also be easier to just remember the actual technique rather than trying to give it some jargonish name. Anyway, as I said above, I think LLMs are a bit better with arguments than definitions, so some elegance might be retained and perhaps you can later refactor to use more elegant definitions as well. (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)
Finally, thanks for bringing up the limitations of LLMs. I also feel that LLMs are probably not currently able to really go beyond their training data, producing new theories with truly novel arguments or definitions. I'm skeptical that we will see a proof of the Riemann hypothesis in near future just drop from an LLM (human utilizing an LLM could be a bit of a different story, but I'm not a number theorist and have no idea whether anyone in the field has any plausible attack vectors currently). They are getting very good at combining and rephrasing existing stuff, however.
> I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems.
If you were using Isabelle/HOL, then (depending on field) you could already have had this. Sledgehammer is pretty powerful, even though it's "just" SAT solvers plus (not-quite-naïve) brute-force. Writes awful proofs (even if half a minute of staring reveals elegant concepts behind it), and can take a very long time to run if you don't have sensible intermediate lemmas (although you'll be writing those anyway, in the course of your work), but if you start at the top of the page and work down, writing "try" in place of every proof, you'll get proofs (or counterexamples) of nearly everything, without putting in any extra work. (This is pre-LLM technology, to be clear: they just have a terrible marketing department.)
There's currently a UI issue where you have to accept the proofs in reverse order (bottom to top), otherwise it goes "oh, something changed!" and wipes the attempts it was making for the later proofs; but that shouldn't be too hard to fix with a non-local cache – and in the meantime, it's quite a minor quirk. On a researcher's laptop (i.e., one considerably more powerful than mine!), it's rare that sledgehammer finds a proof slower than it takes to type out the statement of the next theorem, and the "try" keyword changes background colour to let you know when it's done.
You'll notice I said "sensible intermediate lemmas". You might need to recalibrate your notion of elegance slightly for this, if you want to get fast proofs out the other end – but sledgehammer can work with even totally backwards lemmas like "∀list. list = hd list ## tl list": it'll just use a general-purpose solver rather than a special-purpose one, and so be a lot slower to find proofs. In practice, this is not an issue: it's an easier, more explicable skill than prompt engineering, and Isabelle will mostly just work around you if you do it wrong.
> if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, […])
Note that this is my mathematics reading speed, not my English reading speed. It might not be as impressive as you think. The number of times I've had to go back and re-read four pages because I misunderstood a basic concept…
Well, if I were formalising for the sake of assisting my research, rather than for the joy of formalisation (which, honestly, isn't all that: Isabelle's better than Lean, but it's far from nice), and I just needed a result from the end of a textbook, I'd be very tempted to write:
theorem final_theorem: ‹statement of theorem›
sorry ― ‹TODO: Proven in textbook reference, page 189.›
Isabelle doesn't care. You won't be able to publish it in the Archive of Formal Proofs (a journal of formalised mathematics) because `thm_oracles final_theorem` will say `skip_proof` and the editors will desk-reject it, but sledgehammer will still work fine (provided you put this before the things that require it: that's a mistake you only make once).
> I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition.
Yup! And sometimes different arguments motivate different definitions, and then you end up with a graph of "definition A is easier to prove from definition B than the other way around", which either resolves into a "definition I is the best weak definition for introduction, and definition D is the best strong definition for destruction/elimination", or a circle of equally-valid definitions. (Sadly, I've only encountered the latter in textbooks: never in my own research, however often I've believed I have. But I'm holding out hope!)
> I think LLMs are a bit better with arguments than definitions
So's Isabelle's sledgehammer. Try it? (Again, depending on which field you work in: some things just aren't formalised at all in Isabelle/HOL, so you can't really use them, although a surprising amount is. Given more information, I can give better advice.)
> (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)
Yeah, we call that category theory. The big downside of Isabelle/HOL is that it can't do category theory, because it can't quantify over types: each "argument" has to be written out explicitly, generic over a large (usually infinite) family of use-cases, but not all of them in the way that a dependently-typed logic like Lean can.
But this limitation does make the automation more powerful, so that's actually a good thing for your use-case. I don't understand enough to know how it makes it more powerful, but I imagine it's something like "narrowing the search lets you search deeper". Lean's (currently, and perhaps inherently, inferior) version of sledgehammer has a module that tries to translate Lean expressions into HOL expressions, so it can use some of the techniques available to Isabelle/HOL's sledgehammer. (Some of the Isabelle people have joked that instead of using LLMs, Lean should just bundle a copy of Isabelle/HOL – and while obviously this wouldn't work, it might genuinely work better than LLMs for most use-cases.)
> I also feel that LLMs are probably not currently able to really go beyond their training data, […] They are getting very good at combining and rephrasing existing stuff, however.
I'm concerned that this will lead to increased plagiarism. When Isabelle finds a proof, it tells you where it got it. (That's actually how I learned about the Cantor–Schröder–Bernstein theorem, which finally convinced me that what I was trying to prove was independent of ZF: it told me the name of this theorem, when solving a problem that I didn't think was deeply related to the axiom of choice. All pre-LLM technology, mind!) LLMs (usually (when they succeed)) give you answers, and then do a post-hoc search for where the answers might have come from.
> LLMs have done nothing for "making large scale mechanization viable."
I'm sorry, but this assertion is ridiculous. LLMs absolutely have radically simplified mechanization. Autoformalization of papers using LLM is orders of magnitude faster than doing it manually.
> [...] Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project. Lean’s fantastic (declaration of conflict of interest: I am a maintainer) mathematics library mathlib is only 2.3 million lines of code, and took nine years to write.
LLMs are going to be the basis of total formalization of all ~4M papers in the historical math literature. This project wouldn't be feasible without them.
That's some industrial strength denial you've got going there. Please entertain the possibility that people who are presenting reasoned arguments with evidence against you are not "psychotic". BTW, is Ken Buzzard also psychotic?
Anyway, this avalanche is going to come down on your head whether or not you believe in it. Have fun!
Absolutely that's the reason. But the point is the big communities (I'm thinking https://leanprover-community.github.io/ , Kevin Buzzard and all the stuff he's got going at imperial college in the uk etc, the analogous efforts around roq, agda etc which I'm not as familiar with) have made their respective choices and are just getting on with formalising maths. Then there is a vocal minority who want to sit on the sidelines and say they want all these people to use something different from what they have already decided to use. Seems weird.[1]
But yeah it is definitely easier if you just need to formalise the piece you are working on and not invent the whole universe just to bake an apple pie.
[1] And I know it's exactly the same as the people on here and other forums who say other people should down tools on project X and rewrite it in go/rust/zig/whatever. I find that weird also. Like if you want to rewrite a thing in a different language go do that by all means. But saying someone else who develops something in their own time should instead develop a different thing or use a different language is just weird.
I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.
I think it’s a lot like R vs SAS or Python and not any departure from the norm.
Mathematicians are not highly technical users that generally like programming. If you give them a path of importing someone else’s work they’ll do that instead of redoing it in their theorem prover of choice.
See the old mathematician joke:
A mathematician is asked to make tea. They take the kettle from the shelf, fill it with water, put it on the stove, turn on the heat and boil the water, then pour it into a cup.
The next day someone asks the mathematician to make tea again. The kettle is still on the stove from yesterday and there’s some leftover water in it, enough for tea.
The mathematician dumps the kettle out and puts the it away on the shelf. The mathematician says the system is in a known previously solved state and therefore trivially solved.
Now substitute 1500 lines of coq or lean for the kettle. As far as I know the outputs aren’t interchangeable like a vim or eMacs text file.
> lean4 doesn't let them formalize results outside of zfc.
A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundation, so long as you have an implementation.
Presumably because of potential network effects that would result from everyone being able to work in a single system. I don't think it's strange or implausible for people to want that.
I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen.
This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof.
I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point.
My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier:
$c wff $. $( we use this $constant as a type of formula (well formed formula) $)
$c ( ) ! -> $. $( brackets, negation, implication $)
$v A B C $. $( $variables to be used in formulas $)
wa $f wff A $. $( $floating hypothesis "wa" which says, that A is a well-formed formula $)
wb $f wff B $.
wc $f wff C $.
$( The following assertions define the rules to create formulas $)
$( In Metamath (unlike Metamath Zero), definitions also use the $axiom statement type $)
wng $a wff ! A $. $( "not A is a well-formed-formula" - mandatory hypotheses are (wa) $)
wim $a wff ( A -> B ) $. $( "A implies B is a well-formed-formula" - mandatory hypotheses are (wa, wb) $)
$c |- $. $( this $constant will be used as a type of provable formula $)
$( Schemes of $axioms of propositional logic $)
a1 $a |- ( A -> ( B -> A ) ) $.
a2 $a |- ( ( A -> ( B -> C ) ) -> ( ( A -> B ) -> ( A -> C ) ) ) $.
a3 $a |- ( ( ! A -> ! B ) -> ( B -> A ) ) $.
$( Definition of the Modus Ponens rule of inference in new scope; otherwise $essential hypotheses (inputs) mp1, mp2 will become mandatory for all upcoming assertions $)
${
mp1 $e |- A $.
mp2 $e |- ( A -> B ) $.
mp $a |- B $. $( mandatory hypotheses of "mp" are (wa, wb, mp1, mp2) $)
$}
$( A $proof states the string of symbols to be proven, followed by a list of labels used by the stack machine $)
$( $floating and $essential hypotheses are pushed onto the top of the stack, $axioms and $proofs transform it by using the top of the stack as inputs $)
$( When the stack is empty at the end, the proof is successful, and the proved statement can be reused in further proofs using its label $)
$( " A implies ( B implies C) is a well-formed-formula" $)
formula1 $p wff ( A -> ( B -> C ) ) $= wa wb wc wim wim $.
$( "( A -> A ) -> ( A -> A ) is true (follows from the axioms)" $)
formula2 $p |- ( ( A -> A ) -> ( A -> A ) ) $= wa wa wa wim wim
wa wa wim wa wa wim wim
wa wa a1
wa wa wa a2
mp $.
Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.
Reminds me of the idea of Radical Monopolies from Ivan Illich in a way. If a technology or service becomes so wide spread within society, even though many different versions of the technology or service may exist, a Radical Monopoly means that non users will suffer for their non use. Cars and non drivers in cities are the typical example. And I wonder, whether mathematicians who don't user theorem provers will soon suffer under the tyranny of the theorem provers, whether it be Lean or one of the others.
I immediately thought that’s not totally fair due to the size of the Netherlands vs other countries.
I asked Mistral to do an analysis: nearly zero R^2 for car ownership vs log country area, and it’s the same with proportion of urban population in OECD countries.
Netherlands isn’t very different from peers in car ownership, they just treat cyclists very well it seems.
This is a total tangent, just found it interesting.
As it turns out, people live in cities[1]. The amount of empty space a country has outside of cities doesn't have much bearing on navigation and infrastructure inside cities.
Right, but there’s zero correlation between urban population percentage and cars per capita either, which was surprising to me. I’d have expected a vague logistic curve.
My takeaway was not the involvement of the LLMs, which I consider to be irrelevant; the core was that there was an exploit of a flaw in the verification engine that allowed an incorrect proof to be validated. That is not great.
In addition to their use as tools for pure math, they are also used for software verification, where adversarial examples could have real-world applications in verifiable supply chain attacks.
Metamath (and specifically Metamath Zero) is formally verified.
Right, but the point is as far as I'm aware nobody accidentally found a bug in Lean by proving a theorem in a non adversarial context (and this submission is a link to a discussion at Mathoverflow). Also I think most formal verification is done using Coq and Isabelle/HOL, no?
But I think this has to be judged against an adversarial influx of LLM-assisted pseudomathematics slop vendors. A sorry-free proof in Lean (or Rocq!) whose top-level types check out is not good enough. You gotta check for compiler chicanery in all the private methods.
Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.
Lean's threat model is not that it's designed so you can just take random lean code at face value without even reviewing it or whatever. It's designed to be a proof assistant to help working mathematicians validate proofs and not validate an "honest" incorrect proof. Malicious proofs that have been specifically constructed to exploit the proof system are known to be a possibility and are considered to be bugs that people try to fix, but they are not cause for serious concern.
Haven't seen much about SPARK and why3 recently, combined with frontier LLMs. It would seem easier to progressively prove properties from an actual implementation (going from absence of runtime errors to partial functional proof to full functional proof if you can beau the cost) and only focus the Lean effort on places where why3 (and its menagerie) of SMT provers give up ?
It would also seem highly agent-able since verification is very modular in SPARK.
Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.
What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.
Was genuinely expecting an article about manufacturing methodologies! Very interesting teachable moment for me, I've always wanted to learn more about Set Theory.
Isn't it today/wouldn't it be in the close future relatively trivial to port most of the already formalized results between languages with help of LLMs?
> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean
Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.
I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.
Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).
That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.
I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.
Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is designed to express executable programs, it has a wildly different grain to it than Lean or any other system designed to be used as a general proof assistant from the ground up.
I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.
That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviously, but that's not an expressibility problem, and I wouldn't really equate what remains practical with triviality. With language extensions, you can just kind of do whatever as shown by Liquid Haskell.
I can see the real pain point more being the fact that it's not like a typical proof assistant, and utilizing it as one is going to be unintuitive and strange.
Metamath contributor here! Each proving tool has its pros and cons, but always happy to see Metamath noted :-).
One thing that's cool about Metamath is that the axioms are not built-in. It's true that the most-used system is based on classical logic and ZFC set theory https://us.metamath.org/mpeuni/mmset.html ... but you don't have to use that system. There's a well-maintained database using intuitionistic logic: https://us.metamath.org/ileuni/mmil.html ; on the so-called "New Foundations" (a many-sorted system): https://us.metamath.org/nfeuni/mmnf.html ; on HOL https://us.metamath.org/holuni/mmhol.html ; and you can make your own if you want to.
In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.
This video I made years ago summarizes Metamath: https://www.youtube.com/watch?v=8WH4Rd4UKGE
Metamath is interesting for education in the principles of formal proofs, because:
1. The Metamath Book is self-contained well written, simple introduction.
2. Everything is explicit, nothing is hidden.
3. Because of extremely simple syntax and semantics it's easy write own proof verifier.
The drawbacks are:
1. Non-standard approach to free and bound variables.
2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.
3. Almost no proof automation. No tactics. Long, hard to read proofs.
I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm
There are other forms of logic? is intuitionistic logic as rigorous? fascinating
edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
> if it is weakened, how can you prove the same stuff?
Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.
Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.
Having a weaker base system means you can distinguish more fine grained between statements.
For example, in an intuitionistic setting there is a difference between a set being non-empty and a set having an element.
Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).
I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on the surface to be as an outcome) human beings are different and want different things, and people are productive in different environments. In particular, people who want to formalize results within the standard framework (including zfc) are never really as a group going to care that much that lean4 doesn't let them formalize results outside of zfc.
> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
I don't know about forcing, but there's certainly a long history of emacs users trying to convince vim users that they're wrong. Without loss of generality - the same is true in the other direction of course.
Software devs are more than used to having a multitude of tools at our disposal (text editors, programming languages, Linux distros...), having strong preferences, and engaging in the delicate balancing act of advocating for our favourites while living-and-letting-live as the cosmic ballet goes on. It's part of our culture; I don't think that culture necessarily exists outside. For instance, a common layman question to ask is, "Why are there so many programming languages? Why doesn't everyone just use the same one?" And I don't think mathematicians are immune to this blind spot.
The nearest equivalent to "tooling" in math, traditionally, would be notation I suppose, and mathematicians are accustomed to eventually coalescing around a single standard notation.
> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
That's why emacs has a vim mode[1].
[1] - https://github.com/emacs-evil/evil
Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.
My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.
This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on.
LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our complete garbage, spec and all, and say it's a proof of something.
It's not shocking at all that the people who seem to get any benefit out of LLMs in the proof assistant space are the ones who could have just don't it themselves anyway.
I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a research mathematician could actually use in real time along actual math research. The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, both individually and collaboratively (such as the recent Tau Ceti project).
Anyway, what do you mean by 'say it's a proof of something'? If you mean this in technical sense, there are plenty of examples around where single individuals or small teams have autoformalized theorems with tens or hundreds of thousands of lines Lean code that pass a comparator challenge (so the theorem is correct). If you mean this in the sense that the proof is also a proof in the eyes of humans, so that someone has actually read or understood the proof, I'm willing to acknowledge that in this area there is much work still to do. In my own experience the current LLMs are already very strong at formally proving theorems (with correct semantics), but they are still lacking in writing human-readable math prose based on these formalizations, for instance.
> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that,
Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.)
> Granted their goal was not so much speed as it was elegance,
Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit.
¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough. "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)
(Sorry for the long post, but yours brought me thinking about a bunch of different aspects.)
First of all, I did not mean to downplay elegance at all. I agree that elegance is very important and that math is very much about trying to find elegant ways to think about various problems and phenomena. It also makes math feel more human and art-like, as elegance is not completely objective. And I also agree that LLMs do not seem to currently have consistent mathematical taste. I find they often do quite ugly or unoptimal proofs, although sometimes they also surprise me with a more elegant one than what I had in mind myself. And when we pass from arguments to choosing good definitions or seeing the big picture they are often much worse. Finally, formalization efforts such as Mathlib are very interesting from the elegance point of view. I'd actually be interested to see whether it would be possible to do lecture notes or textbooks based on Mathlib, written in standard math prose so that wider crowd of mathematicians might benefit from the insights that people had while formalizing.
However, as a research mathematician, I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. These formalized versions are at least at the moment not going to have pretty proofs, and the proofs the LLM comes up with might even be different from what I'm writing in the paper (but probably in practice not very different if I'm formalizing every lemma). Still, if this can be done quickly enough, I think the result could be net positive even if the formalizations never leave my local hard drive: I will have confidence that I did not miss an edge case in the statements, where usually double-checking these things is actually a very time-consuming part of writing a paper. Thus I might be able to produce papers with less mistakes (usually non-important ones but they do happen). In this sort of workflow speed matters, and if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, and I do not mean this sarcastically!).
Returning a bit to the topic of elegance, I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition. There might also be some difference in how well this works out in practice in different fields. At least historically people in analysis (like myself) are happy to repeat known arguments in slightly different settings. It could be hard to make a version that works in every setting because different sets of assumptions could allow for a similar argument to work. Or it could also be easier to just remember the actual technique rather than trying to give it some jargonish name. Anyway, as I said above, I think LLMs are a bit better with arguments than definitions, so some elegance might be retained and perhaps you can later refactor to use more elegant definitions as well. (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)
Finally, thanks for bringing up the limitations of LLMs. I also feel that LLMs are probably not currently able to really go beyond their training data, producing new theories with truly novel arguments or definitions. I'm skeptical that we will see a proof of the Riemann hypothesis in near future just drop from an LLM (human utilizing an LLM could be a bit of a different story, but I'm not a number theorist and have no idea whether anyone in the field has any plausible attack vectors currently). They are getting very good at combining and rephrasing existing stuff, however.
> I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems.
If you were using Isabelle/HOL, then (depending on field) you could already have had this. Sledgehammer is pretty powerful, even though it's "just" SAT solvers plus (not-quite-naïve) brute-force. Writes awful proofs (even if half a minute of staring reveals elegant concepts behind it), and can take a very long time to run if you don't have sensible intermediate lemmas (although you'll be writing those anyway, in the course of your work), but if you start at the top of the page and work down, writing "try" in place of every proof, you'll get proofs (or counterexamples) of nearly everything, without putting in any extra work. (This is pre-LLM technology, to be clear: they just have a terrible marketing department.)
There's currently a UI issue where you have to accept the proofs in reverse order (bottom to top), otherwise it goes "oh, something changed!" and wipes the attempts it was making for the later proofs; but that shouldn't be too hard to fix with a non-local cache – and in the meantime, it's quite a minor quirk. On a researcher's laptop (i.e., one considerably more powerful than mine!), it's rare that sledgehammer finds a proof slower than it takes to type out the statement of the next theorem, and the "try" keyword changes background colour to let you know when it's done.
You'll notice I said "sensible intermediate lemmas". You might need to recalibrate your notion of elegance slightly for this, if you want to get fast proofs out the other end – but sledgehammer can work with even totally backwards lemmas like "∀list. list = hd list ## tl list": it'll just use a general-purpose solver rather than a special-purpose one, and so be a lot slower to find proofs. In practice, this is not an issue: it's an easier, more explicable skill than prompt engineering, and Isabelle will mostly just work around you if you do it wrong.
> if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, […])
Note that this is my mathematics reading speed, not my English reading speed. It might not be as impressive as you think. The number of times I've had to go back and re-read four pages because I misunderstood a basic concept…
Well, if I were formalising for the sake of assisting my research, rather than for the joy of formalisation (which, honestly, isn't all that: Isabelle's better than Lean, but it's far from nice), and I just needed a result from the end of a textbook, I'd be very tempted to write:
Isabelle doesn't care. You won't be able to publish it in the Archive of Formal Proofs (a journal of formalised mathematics) because `thm_oracles final_theorem` will say `skip_proof` and the editors will desk-reject it, but sledgehammer will still work fine (provided you put this before the things that require it: that's a mistake you only make once).> I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition.
Yup! And sometimes different arguments motivate different definitions, and then you end up with a graph of "definition A is easier to prove from definition B than the other way around", which either resolves into a "definition I is the best weak definition for introduction, and definition D is the best strong definition for destruction/elimination", or a circle of equally-valid definitions. (Sadly, I've only encountered the latter in textbooks: never in my own research, however often I've believed I have. But I'm holding out hope!)
> I think LLMs are a bit better with arguments than definitions
So's Isabelle's sledgehammer. Try it? (Again, depending on which field you work in: some things just aren't formalised at all in Isabelle/HOL, so you can't really use them, although a surprising amount is. Given more information, I can give better advice.)
> (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)
Yeah, we call that category theory. The big downside of Isabelle/HOL is that it can't do category theory, because it can't quantify over types: each "argument" has to be written out explicitly, generic over a large (usually infinite) family of use-cases, but not all of them in the way that a dependently-typed logic like Lean can.
But this limitation does make the automation more powerful, so that's actually a good thing for your use-case. I don't understand enough to know how it makes it more powerful, but I imagine it's something like "narrowing the search lets you search deeper". Lean's (currently, and perhaps inherently, inferior) version of sledgehammer has a module that tries to translate Lean expressions into HOL expressions, so it can use some of the techniques available to Isabelle/HOL's sledgehammer. (Some of the Isabelle people have joked that instead of using LLMs, Lean should just bundle a copy of Isabelle/HOL – and while obviously this wouldn't work, it might genuinely work better than LLMs for most use-cases.)
> I also feel that LLMs are probably not currently able to really go beyond their training data, […] They are getting very good at combining and rephrasing existing stuff, however.
I'm concerned that this will lead to increased plagiarism. When Isabelle finds a proof, it tells you where it got it. (That's actually how I learned about the Cantor–Schröder–Bernstein theorem, which finally convinced me that what I was trying to prove was independent of ZF: it told me the name of this theorem, when solving a problem that I didn't think was deeply related to the axiom of choice. All pre-LLM technology, mind!) LLMs (usually (when they succeed)) give you answers, and then do a post-hoc search for where the answers might have come from.
> LLMs have done nothing for "making large scale mechanization viable."
I'm sorry, but this assertion is ridiculous. LLMs absolutely have radically simplified mechanization. Autoformalization of papers using LLM is orders of magnitude faster than doing it manually.
To quote Ken Buzzard (of the Xena Project):
https://xenaproject.wordpress.com/2026/07/20/human-mathemati...
> [...] Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project. Lean’s fantastic (declaration of conflict of interest: I am a maintainer) mathematics library mathlib is only 2.3 million lines of code, and took nine years to write.
LLMs are going to be the basis of total formalization of all ~4M papers in the historical math literature. This project wouldn't be feasible without them.
What is absurd is evaluating something on the lines of code it produces. AI psychosis at work.
That's some industrial strength denial you've got going there. Please entertain the possibility that people who are presenting reasoned arguments with evidence against you are not "psychotic". BTW, is Ken Buzzard also psychotic?
Anyway, this avalanche is going to come down on your head whether or not you believe in it. Have fun!
I have zero experience with formal verification, just speculating here - but could it be because of the network effects?
More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?
Absolutely that's the reason. But the point is the big communities (I'm thinking https://leanprover-community.github.io/ , Kevin Buzzard and all the stuff he's got going at imperial college in the uk etc, the analogous efforts around roq, agda etc which I'm not as familiar with) have made their respective choices and are just getting on with formalising maths. Then there is a vocal minority who want to sit on the sidelines and say they want all these people to use something different from what they have already decided to use. Seems weird.[1]
But yeah it is definitely easier if you just need to formalise the piece you are working on and not invent the whole universe just to bake an apple pie.
[1] And I know it's exactly the same as the people on here and other forums who say other people should down tools on project X and rewrite it in go/rust/zig/whatever. I find that weird also. Like if you want to rewrite a thing in a different language go do that by all means. But saying someone else who develops something in their own time should instead develop a different thing or use a different language is just weird.
I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.
I think it’s a lot like R vs SAS or Python and not any departure from the norm.
Mathematicians are not highly technical users that generally like programming. If you give them a path of importing someone else’s work they’ll do that instead of redoing it in their theorem prover of choice.
See the old mathematician joke:
A mathematician is asked to make tea. They take the kettle from the shelf, fill it with water, put it on the stove, turn on the heat and boil the water, then pour it into a cup.
The next day someone asks the mathematician to make tea again. The kettle is still on the stove from yesterday and there’s some leftover water in it, enough for tea.
The mathematician dumps the kettle out and puts the it away on the shelf. The mathematician says the system is in a known previously solved state and therefore trivially solved.
Now substitute 1500 lines of coq or lean for the kettle. As far as I know the outputs aren’t interchangeable like a vim or eMacs text file.
> lean4 doesn't let them formalize results outside of zfc.
A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundation, so long as you have an implementation.
Presumably because of potential network effects that would result from everyone being able to work in a single system. I don't think it's strange or implausible for people to want that.
https://github.com/Syzygies/Compare
I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen.
This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof.
https://github.com/Syzygies/Compare/blob/main/source/lean/Na...
I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point.
Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m...
Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0
How do other proof systems compare?
Some bug counts: https://tristan.st/blog/in_search_of_falsehood
According to [0], "Rocq’s kernel spans approximately 41K lines of OCaml code, while Lean’s kernel consists of approximately 8K lines of C++ code."
[0] https://dl.acm.org/doi/pdf/10.1145/3747511
My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier:
Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.
How would you improve it? (Also note that this is not the language mathematicians actually work with - that's more like https://www.youtube.com/watch?v=b-RfoUuQpAQ)
Similarly, for Metamath Zero, MM1 compiles down to the MM0 base language: https://www.youtube.com/watch?v=A7WfrW7-ifw
I think it's just a neat example that helps one understand how the verifier itself works at the most fundamental level.
Or Raku.
Reminds me of the idea of Radical Monopolies from Ivan Illich in a way. If a technology or service becomes so wide spread within society, even though many different versions of the technology or service may exist, a Radical Monopoly means that non users will suffer for their non use. Cars and non drivers in cities are the typical example. And I wonder, whether mathematicians who don't user theorem provers will soon suffer under the tyranny of the theorem provers, whether it be Lean or one of the others.
> Cars and non drivers in cities are the typical example.
Have a look at Dutch cities for how to avoid this.
I immediately thought that’s not totally fair due to the size of the Netherlands vs other countries.
I asked Mistral to do an analysis: nearly zero R^2 for car ownership vs log country area, and it’s the same with proportion of urban population in OECD countries.
Netherlands isn’t very different from peers in car ownership, they just treat cyclists very well it seems.
This is a total tangent, just found it interesting.
As it turns out, people live in cities[1]. The amount of empty space a country has outside of cities doesn't have much bearing on navigation and infrastructure inside cities.
[1] https://xkcd.com/1138/
Right, but there’s zero correlation between urban population percentage and cars per capita either, which was surprising to me. I’d have expected a vague logistic curve.
So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.
https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions
My takeaway was not the involvement of the LLMs, which I consider to be irrelevant; the core was that there was an exploit of a flaw in the verification engine that allowed an incorrect proof to be validated. That is not great.
In addition to their use as tools for pure math, they are also used for software verification, where adversarial examples could have real-world applications in verifiable supply chain attacks.
Metamath (and specifically Metamath Zero) is formally verified.
Right, but the point is as far as I'm aware nobody accidentally found a bug in Lean by proving a theorem in a non adversarial context (and this submission is a link to a discussion at Mathoverflow). Also I think most formal verification is done using Coq and Isabelle/HOL, no?
But I think this has to be judged against an adversarial influx of LLM-assisted pseudomathematics slop vendors. A sorry-free proof in Lean (or Rocq!) whose top-level types check out is not good enough. You gotta check for compiler chicanery in all the private methods.
Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.
This is something that people have thought about a fair bit and that link does not mean what you think it means
https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Lean's threat model is not that it's designed so you can just take random lean code at face value without even reviewing it or whatever. It's designed to be a proof assistant to help working mathematicians validate proofs and not validate an "honest" incorrect proof. Malicious proofs that have been specifically constructed to exploit the proof system are known to be a possibility and are considered to be bugs that people try to fix, but they are not cause for serious concern.
Haven't seen much about SPARK and why3 recently, combined with frontier LLMs. It would seem easier to progressively prove properties from an actual implementation (going from absence of runtime errors to partial functional proof to full functional proof if you can beau the cost) and only focus the Lean effort on places where why3 (and its menagerie) of SMT provers give up ?
It would also seem highly agent-able since verification is very modular in SPARK.
I had not been familiar with the term "Dumey microsecond".
For those who found it interesting, perhaps you will also find this term enjoyable https://en.wikipedia.org/wiki/Kairos for its similarity.
Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.
What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.
[1] https://fstar-lang.org/
[2] https://fstarlang.github.io/lowstar/html/Introduction.html
Was genuinely expecting an article about manufacturing methodologies! Very interesting teachable moment for me, I've always wanted to learn more about Set Theory.
Recently I was playing around in this space and came across Dafny, rather I should confess that Claude code pointed be to it.
For software projects it seemed very approachable, even for a complete newbie like me. Probably not for Math though.
Isn't it today/wouldn't it be in the close future relatively trivial to port most of the already formalized results between languages with help of LLMs?
> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean
Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.
I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.
Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).
That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.
1. https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf
I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.
Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.
It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.
Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is designed to express executable programs, it has a wildly different grain to it than Lean or any other system designed to be used as a general proof assistant from the ground up.
I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.
That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviously, but that's not an expressibility problem, and I wouldn't really equate what remains practical with triviality. With language extensions, you can just kind of do whatever as shown by Liquid Haskell.
I can see the real pain point more being the fact that it's not like a typical proof assistant, and utilizing it as one is going to be unintuitive and strange.
https://hackage.haskell.org/package/type-settheory