7 ms·
Are We Stuck with Lean?
- 7373737373 3mo agoMetamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/mmverify.py 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 https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood https://tristan.st/blog/in_search_of_falsehood
- 7373737373 3mo agoMy 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 $.
- seanhunter 3mo agoFair 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.
- 7373737373 3mo agoHow 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 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 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.
- jjgreen 3mo agoOr Raku.
- wk_end 3mo agoAccording 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 https://dl.acm.org/doi/pdf/10.1145/3747511
- ux266478 3mo ago> 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.
- eru 3mo agoI 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.
- solomonb 3mo agoCorrect. 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 https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf
- ux266478 3mo agoI 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.
- solomonb 3mo agoIdris 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.
- dwheeler 3mo agoMetamath 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 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 https://us.metamath.org/ileuni/mmil.html ; on the so-called "New Foundations" (a many-sorted system): https://us.metamath.org/nfeuni/mmnf.html https://us.metamath.org/nfeuni/mmnf.html ; on HOL https://us.metamath.org/holuni/mmhol.html 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 https://www.youtube.com/watch?v=8WH4Rd4UKGE
- ux266478 3mo agoWhat 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 https://github.com/digama0/HOL
- xelxebar 3mo agoYeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm https://github.com/metamath/set.mm/blob/develop/hol.mm
- 3mo ago
- IsTom 3mo agoSo that link(https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.
- HappyPanacea 3mo agohttps://lipn.info/@mevenlennonbertrand/116997927457012577 https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions
- andrewla 3mo agoMy 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.
- HappyPanacea 3mo agoRight, 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?
- Diogenesian 3mo agoBut 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.
- seanhunter 3mo agoI 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.
- ux266478 3mo ago> 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.
- quasisphere 3mo agoAgreed. 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.
- 3mo ago
- knuckleheads 3mo agoReminds 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.
- eru 3mo ago> Cars and non drivers in cities are the typical example. Have a look at Dutch cities for how to avoid this.
- data-ottawa 3mo agoI 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.
- applfanboysbgon 3mo agoAs 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/ https://xkcd.com/1138/
- data-ottawa 3mo agoRight, 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.
- 3mo ago
- ducktective 3mo agoRecent 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/ https://fstar-lang.org/ [2] https://fstarlang.github.io/lowstar/html/Introduction.html https://fstarlang.github.io/lowstar/html/Introduction.html
- deleted 3mo ago[deleted]
- dieselgate 3mo agoWas genuinely expecting an article about manufacturing methodologies! Very interesting teachable moment for me, I've always wanted to learn more about Set Theory.
- Syzygies 3mo agohttps://github.com/Syzygies/Compare 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/Natural%20Number%20Game/proofs.png 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.
- yumraj 3mo agoRecently 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.
- or_am_i 3mo agoIsn'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?
- godwinson__4-8 3mo agoI 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 https://en.wikipedia.org/wiki/Kairos for its similarity.
- touisteur 3mo agoHaven'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.
- HawtAds 3mo agoI don't see what the issue is. Isn't the entire point of LLMs that we can easily translate between languages? What better way to cross check the correctness of a proof than to run it on several different systems simultaneously.
- deterministic 3mo agoNo programming language will ever be perfect. But it's still better for everyone to focus on improving one language than to recreate the same ideas across dozens of different languages, like a Tower of Babel of duplicated effort.
- eru 3mo agoAre you programming in Fortran?
- deterministic 3mo agoThat's a bad analogy. LEAN is a leading bleeding edge proof verification tool.
- eru 2mo agoFortran used to be the only programming language (and even cutting edge by default). People went off and created new ones anyway.
- deterministic 2mo agoAnd maybe somebody will create something better than LEAN. That has nothing to do with the original argument.
- deleted 2mo ago[deleted]