11 ms·

The Math Is Haunted

409 points by danabramov 1y ago

7373737373 1y ago
One problem I have with learning Lean is that tactics - like rfl in the example - are overloaded, and their full semantics not completely explained/understandable from the tutorials. Unlike, say, C programming where one may understand what happens to the program state down to the bit, it feels too fuzzy. And the rewrite (rw) tactic syntax doesn't feel natural either.
- danabramov 1y ago
  Yeah the documentation is also quite fragmented because tactics are user-definable and some are from Lean vs from Mathlib etc. I've gotten quite decent at using the basic ones but I still sometimes ask on Zulip if something isn't working as I expected.
- LegionMammal978 1y ago
  Yeah, I've similarly found the tactics in Coq (now Rocq) difficult to internalize. E.g., I might have "A = B" and "P(A,A)" available, and I want to conclude "P(A,B)", but the rewrite will fail for some arcane reason. (Issues with the definition of some of the intermediate structures, I'd imagine.) On the other end of the spectrum, I've recently been playing with Metamath and its set.mm database, which has no programmable tactics at all, only concrete inferences that can be used in a proof. (E.g., the modus ponens inference ax-mp says that "|- ph" and "|- ( ph -> ps )" prove "|- ps", where "ph" and "ps" are variables that can be substituted.) Alas, it's not much better, since now you have to memorize all the utility lemmas you might need!
  - 7373737373 1y ago
    Agreed - the Metamath base language (and its verifier) seem to be the most tractable of all I've seen, although it is probably still quite far away from the complexity of the high level language(s) that compile to it. Derived from it, the currently best attempt to achieve an unambiguous and secure language seems to be Metamath Zero: https://github.com/digama0/mm0 https://github.com/digama0/mm0
- solomonb 1y ago
  This is why I prefer Agda, where everything comes down to pattern matching.
  - agnishom 1y ago
    You can absolutely use pattern matching in Lean instead of tactics, if you prefer to write the proof that is closer to "what is going on under the hood"
    - solomonb 1y ago
      yeah i didn't mean to imply you cannot do that, but tactics seem to be highly encouraged. I'm actually a big fan of Lean, I just like it more as a programming language for writing programs with dependent types then as a proof checker.
- gylterud 1y ago
  This is one of the reasons I prefer Agda. It is usually written without tactics, you just write the proof term in a functional programming language via the Curry–Howard correspondence. The trade off is that you must be more disciplined with creating useful abstractions and functions, otherwise proving even routine stuff becomes really tedious.
  - Paracompact 1y ago
    I'm not sure you prefer Agda so much as you prefer providing proof terms functionally rather than imperatively. Then again I've never used Agda; how does it differ from Coq/Rocq minus Ltac or Lean minus tactics?
    - logicchains 1y ago
      Coq has much less support for working with dependent types; you need lots of annotations compared to Agda (which has superior dependent pattern matching support). Lean is somewhere between the two.
- kmill 1y ago
  At least you can 'go to definition' on the tactics and see what they're doing. It's a lot to take in at the beginning, but it can all be inspected and understood. (At least until you get to the fundamental type theory; the reduction rules are a lot harder to get into.) > the rewrite (rw) tactic syntax doesn't feel natural either. Do you have any thoughts on what a natural rewrite syntax would be?
  - 7373737373 1y ago
    > Do you have any thoughts on what a natural rewrite syntax would be? Not yet, but I'd probably prefer something that more explicitly indicated (in English, or some sort of more visually "pointing" indicator) which specific parts of the previous step would be replaced It feels weird, or I'd have to get used to that both what is being replaced and what it is replaced with depends on some distant context, it's very indirect as it requires switching attention between the tactics tree and the context or previous proofs
    - danabramov 1y ago
      If you have specific ideas, I'm also curious! I wonder if Lean can be extended to support what you're thinking of — its ability to have custom syntax and tactics seems really powerful. That's part of what excites me about Lean as I'm also not always the biggest fan of existing tactics, but they seem to evolve similarly to other pieces of software.
      - kmill 1y ago
        We're working on a new rewrite tactic this summer at the Lean FRO (I don't know if I ever directly mentioned that to you yet on Zulip). One interface I'm planning on is `rw [(pos := 1,3,2) thm]` to be able to navigate to the place where the rewrite should occur, with a widget interface to add these position strings by clicking on them in the Infoview. The whole occurrences interface will also be revamped, and maybe someone from the community could help make a widget interface for that too. Of course there's already `conv => enter [1,3,2]; rw thm`, but putting it directly into `rw` is more convenient while also being more powerful (`conv` has intrinsic limitations for which positions it can access). The interface is what people will notice, but technical idea of the project is to separate the "what" you want to rewrite from "how" to get dependent type theory to accept it, and then make the "how" backend really good at getting rewrites to go through. No more "motive not type correct", but either success or an error message that gives precise explanations of what went wrong with the rewrite. And, yeah, it's great that Lean lets you write your own tactics, since it lets people write domain-specific languages just for solving the sorts of things they run into themselves. There's no real difference between writing tactics as a user or as part of the Lean system itself. Anyone could make a new rewrite tactic as a user package.
- swagmoney1606 1y ago
  You may like Agda. I prefer Lean even though you are right about this.
- emmelaich 1y ago
  It was interesting to me as it didn't fit my expectations. As a math theory ignoramus, I expected that reflection and rewrite are more fundamental than addition. But Lean seems to assume addition but require explicit rfl and rewrite. Perhaps there's a Lean "prelude" that does it for you.
  - derdi 1y ago
    Yes, there is a prelude that defines natural numbers and an addition function on them. As the post notes, the reflexivity tactic "unfolds" the addition, meaning that it applies the addition function to the constants it is given, to arrive at a constant. This is not specific to addition, it unfolds other function definitions too. So addition doesn't have to come first, you are right that reflexivity is more fundamental.
    - danabramov 1y ago
      Author here — this is correct. I’ve added a paragraph on this in an edit btw so it’s possible the parent poster hasn’t seen it yet. Reproducing the paragraph: (Here, rfl closes ⊢ 3 + 3 = 6, but for a different reason than one might think. It doesn’t really “know” that 3 + 3 is 6. Rather, rfl unfolds the definitions on both sides before comparing them. As 3, 6, and + get unfolded, both sides turn into something like Nat.zero.succ.succ.succ.succ.succ.succ. That’s why it actually is a something = something situation, and rfl is able to close it.) Also, another resource on this is https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/ https://xenaproject.wordpress.com/2019/05/21/equality-part-1...
      - emmelaich 1y ago
        Thanks! That makes sense.
  - armchairhacker 1y ago
    It's because the addition can evaluate to only one form: `3 + 3` and `6` both evaluate to `succ (succ (succ (succ (succ (succ zero)))))`, similarly Lean can infer `4 * 3 = 1 + 3 + 8` because both evaluate to the same as `12`. But an expression can be rewritten to an infinite number of forms, e.g. `x * 2` can be rewritten to `x + x`, `(x + (x / 2)) * 4/3)`, etc. So `refl` can automatically evaluate both sides but not rewrite them.
- gowld 1y ago
  One thing Lean inherits from mathematics is the use of opaque notation. It would be nice to inherit some readability from programming. Paperproof is an effort in one direction (visualization of the logic tree) https://paperproof.brick.do/lean-coq-isabel-and-their-proof-trees-yjnd2O2RgxwV https://paperproof.brick.do/lean-coq-isabel-and-their-proof-...
- daxfohl 1y ago
  The surprising thing to me was that tactics are all written in "user-level" code, outside the proof kernel. This makes sense in the sense that you want a small, thoroughly tested kernel that doesn't change. But it also implies that if you use tactics in your proof, then your proof can go from correct to failing if one of the tactics you use gets modified between releases. Is that a problem in real world use?
  - Tainnor 1y ago
    Yes. I've seen proofs fail after a mathlib update because the behaviour of simp changed. I've never seen it do less after an update (so far), but sometimes it'll simplify more and then the next steps may fail to work. I've since adopted the suggestion (that is afaik used in mathlib) to never use bare simp unless it closes the current goal directly. Instead, if you write simp?, Lean will run the simplifier and tell you exactly which theorems it used (in the form of simp only [...]) which you can then insert into the proof instead.
    - daxfohl 1y ago
      I guess it makes sense: the tactics are defined in the lean repo (but not in the kernel of that repo), while mathlib has its own repo. But any changes to tactic code triggers a test to verify that mathlib still works against it. Which implies there's a reasonable set of checks and balances that don't allow tactic changes to break anything too badly if you follow mathlib's idioms, though it can still happen.
- Tainnor 1y ago
  I understand what you mean, but I shudder to think at how complicated it would be to write certain proofs without tactics, e.g. simp, ring, omega, linarith and friends all really do a lot of work.
kevinqi 1y ago
as someone who hasn't seen Lean before but was curious from alphaproof, love the intro! curious if you can mention what you're working on in Lean?
- danabramov 1y ago
  For now I'm just learning math with it! Currently I'm going through https://github.com/teorth/analysis https://github.com/teorth/analysis (Tao's Lean companion to his textbook) and filling in the `sorry`s in the exercises (my solutions are in https://github.com/gaearon/analysis-solutions https://github.com/gaearon/analysis-solutions).
  - kevinqi 1y ago
    very cool. btw, I also love that "sorry" is the "any" equivalent in Lean
7373737373 1y ago
Does Lean have some sort of verification mode for untrusted proofs that guarantees that a given proof certainly does not use any "sorry" (however indirectly), and does not add to the "proving power" of some separately given fixed set of axioms with further axioms or definitions?
- jonny_eh 1y ago
  Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355 https://github.com/leanprover/lean3/issues/1355
  - kmill 1y ago
    That's Lean 3, from eight years ago, and it's from before 'sorry' really existed in the way we know it now. --- To answer the GP's question: Not only is there a verification mode, but Lean generates object files with the fully elaborated definitions and theorems. These can be rechecked by the kernel, or by external verifiers. There's no need to trust the Lean system itself, except to make sure that the theorem statements actually correspond to what we think they're supposed to be.
    - treyd 1y ago
      What exactly do these object files look like?
      - kmill 1y ago
        The "olean" files are a binary format that contain everything that was added to the Lean environment. Among other things, it includes all of the declarations and their Lean.Expr [1] expressions. People have written tools to dump the data for inspection [2], or to independently check that the expressions are type correct and the environment is well-formed (that is, check the correctness). [1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd454711e2f9e4e20cbbde47ba85/src/Lean/Expr.lean#L302 https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib
deleted 1y ago
[deleted]
cubefox 1y ago
One thing I didn't know until recently was that Lean doesn't solve the problem of verifying that a formal theorem actually states what we think it states rather than something else. In some cases that's not an issue, because the formal statement of the theorem is very simple. E.g. for Fermat's Last Theorem, which can be formally expressed with "(x y z : ℕ+) (n : ℕ) (hn : n > 2) : x^n + y^n ≠ z^n". But in other cases it might be much harder to verify that a formal statement actually matches the intuitive informal statement we want. Of course, Lean or similar languages still offer the huge potential of verifying that a formal statement is provable, even if they don't help with verifying that the formal statement matches the intended informal statement in natural language.
- danabramov 1y ago
  Are there, in general, ways to do that? Sorry if this sounds like a troll question, but I struggle to think of how one would verify that a formal statement matches the accepted understanding other than painstakingly going through the definitions with experts from both sides.
  - cubefox 1y ago
    I don't think there is any technical solution for that, apart perhaps from asking an LLM, or multiple different LLMs, whether it thinks the formal definition matches the informal statement. When mathematicians check normal (informal) proofs they usually verify both things at once: that the proof doesn't contain mistakes or insufficiencies, and that it proves what the author says it proves. Formal proof checkers aren't able to do the latter.
    - danabramov 1y ago
      I personally view proof checkers as mathematicians' tools so I assume mathematicians would be involved either way. With some percentage actually preferring to work closely with these tools. See also Terence Tao's comment in https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/#comment-688326 https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t... which feels relevant to me
brookst 1y ago
I’ve been kicking around the idea of something like Lean (maybe even just Lean?) to rewrite news and other non-fiction articles, treating statements as theorems that need to be proven. Proofs could include citations, and could be compound things like “this is a fact if three of my approved sources asserted it as a fact” It should then be possible to get a marked-up version of any document with highlighting for “proven” claims. Sure, it’s not perfect, but I think it would be an interesting way to apply the rigor that used to be the job of publications.
- ants_everywhere 1y ago
  I don't know why you're getting downvoted because I think this is an interesting idea. Completely impossible but still interesting and fun to explore. But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples
  - ramses0 1y ago
    Basically [Citation Needed]
  - almostgotcaught 1y ago
    [flagged]
    - riku_iki 1y ago
      But such system exists, mostly implemented in prolog.
      - ants_everywhere 1y ago
        Does it actually?
        kevindamm 1y ago
        The first thing this thread made me think of: https://cyc.com/ https://cyc.com/ It's been around for decades.. I'm sure there are other similar systems.
Waterluvian 1y ago
Wait… so are we basically compiling a dictionary of proofs all stemming from a handful of self-evident truths? And every further proof is just some logical aggregation of previous proofs? Can someone please turn this into a Zachtronics style game?! I badly, direly want this. There’s a game called Euclidea that’s kind of like this for trigonometry and the whole premise of building a tower of logic is deeply attractive to me. Is this what pure math is about? Is this what people who become math profs are feeling in their soul? The sheer thrill of adding to that dictionary of proofs? Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
- danabramov 1y ago
  Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.
- hobs 1y ago
  You probably are vaguely referencing the Principa Mathematica.
  - Tainnor 1y ago
    That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.
- treyd 1y ago
  You might be thinking of Euclid's axioms, which defines points, lines, planes, etc, and that lines can be parallel. This is an interesting one because the system is violated if your space is not flat, like if you're on a sphere. You could also be thinking of Zermelo-Fraenknel set theory (ZF/ZFC), which most of modern mathematics is ultimately based upon.
  - deleted 1y ago
    [deleted]
andoando 1y ago
Is there a standard library/repository of all existing mathematical proofs one can add to?
- ants_everywhere 1y ago
  There are a few. The lean one is at https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4
DoctorOetker 1y ago
I possess a proof of FLT, and will publish the metamath formalization, in due time (first I need to build a secure display, for reasons that will become clear).
- olddustytrail 1y ago
  Fermat's Last Theorem is easily solved with css. Just do: margin-left: 200px; and you're sorted.
  - DoctorOetker 1y ago
    people jest, but they will jest less once they think a little more critically: how can cryptography experts expound the security of such and such cryptographic primitives involving discrete numbers, exponentiation, ... but be unable to come up with alternative proofs of FLT? ... but be unable to individually formalize existing supposed proof of FLT? ... but be unable to find a more succinct proof of FLT? who knows their way around the block, if the consensus is that Fermat did not possess a proof but Wiles did finally find a proof, who knows their way around the block, if a much more succinct proof than Wiles long-winded-anc-to-this-date-not-formally-verified-proof? would you jest less?
    - olddustytrail 1y ago
      I probably wouldn't. I'm in a jovial mood and I've managed to joke about many of the worst parts of my life. There are many worse things happening in the world than issues in mathematics. You seem in a serious mood but these things too shall pass.
      - DoctorOetker 1y ago
        > There are many worse things happening in the world than issues in mathematics. But mathematics in general and cryptography in specific, and the canon / propaganda that surrounds it is intimately affecting the principal variation of the same events you so lament.
    - 1y ago
nowittyusername 1y ago
I wonder suppose you are not relying on any tricks or funky shenanigans. is it possible to just throw random stuff at Lean and find interesting observations based if it approves? like use an automated system or an llm that tries all types of wild proofs/theories? and sees if it works? maybe im asking wrong questions though or not stating it well.. this is above my understanding, i could barely get my head around prolog.
- Paracompact 1y ago
  As someone who does certified programming professionally, I believe generative AI and formal methods are a match made in heaven. I might even go so far as to wager that the notion that human programmers will or will not be replaced by LLM-based AI is entirely dependent on whether these AI can get good at certified programming + compositional reasoning. > is it possible to just throw random stuff at Lean and find interesting observations based if it approves? Traditional AI has an easy time with checkers, because the search space is small. Chess is a little harder. Go still cannot be reasonably tackled by non-machine learning AI. Meanwhile, the search space (number of available moves together with the diversity of explorable states) for a sophisticated formal language becomes unfathomably large. When the problem is known to be of a certain nature, often you can time-efficiently brute force it via SMT solvers. Traditionally SMT solvers and proof assistants have been separate branches of formal methods, but they're finally learning to play off each other's strengths (cf. Sledgehammer, Lean-SMT). > like use an automated system or an llm that tries all types of wild proofs/theories? and sees if it works? Research in this vein needs to be made more mainstream. I'm excited, though, that there have been big funders behind these ideas for years now, even before LLMs became big. Cf. "Learning to Find Proofs and Theorems by Learning to Refine Search Strategies" for earlier work, or DeepSeek-Prover for more recent attempts. I'm no machine learning expert, but it seems it's still a very open question how to best train these things and what their future potential is. All in all mainstream LLMs are still rather mediocre at languages like Rocq and Lean. And when they're wrong, their proof scripts are extremely tedious to try to troubleshoot and correct. But I have hope AI tooling in formal methods will mature greatly over time.
  - benreesman 1y ago
thresholds 1y ago
Paging Terrence Howard
ljlolel 1y ago
Maybe before we have AGI we should get an AI that can translate Andrew’s proof into Lean for us. Easily tractable, checkable, useful, and build-upon-able
- grumbelbart2 1y ago
  Work is already underway in that direction: https://github.com/deepseek-ai/DeepSeek-Prover-V2 https://github.com/deepseek-ai/DeepSeek-Prover-V2 but also https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/ https://deepmind.google/discover/blog/alphaevolve-a-gemini-p... Terence Tao is doing a lot of work in this direction.
- zozbot234 1y ago
  Kevin Buzzard is reportedly working on formalizing a modern proof of FLT. This effort has already managed to surface some unsound arguments in one of the prereqs for the proof (namely crystalline cohomology) https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ https://xenaproject.wordpress.com/2024/12/11/fermats-last-th... though the issue has since been fixed.
Karliss 1y ago
Is there a way to read lean proofs noninteractively. After playing with the natural number a game a bit, proofs quickly ended up being opaque sequences of "rw [x]" commands which felt unreadable. It's nice that the editor allows interactively viewing the state at different points, but having to click on each line ruins the flow of reading. Imagine if you had to read python code which has no indentation, braces or anything similar and only way to know where if statement ends or an else block starts is by clicking on each line. My impression might be influenced by the limited vocabulary that the early levels of natural number game provides. Does the richer toolset provided by full lean make it easier to make proofs readable without requiring you to click on each line to get the necessary context?
- RossBencina 1y ago
  > Is there a way to read lean proofs noninteractively. I'd like to see an answer to this question. I was looking into it the other day. I found this: https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ Which gives a way to do the clicking-through outside the editor. And maybe gives some insight into how Lean people see things.
- danabramov 1y ago
  This is a great question! I’m still not very experienced so take it with a grain of salt. But here’s my take on it. I’ve been spending time with Lean quite a bit for the past few months. When I look at a proof, I don’t “read” it the same way as I do with programming. It feels a bit more like “scanning”. What stands out is the overall structure of the argument, what tactics are used, and what lemmas are used. In real Lean code, the accepted style is to indent any new goals, work on one goal at a time (except a few special parallel tactics), and outdent when the goal is done. That’s what I mean by the “shape” of the argument. See some examples in this PR I’m working on: https://github.com/gaearon/analysis-solutions/pull/7/files https://github.com/gaearon/analysis-solutions/pull/7/files Once you’re familiar with what tactics do, you can infer a lot more. For example `intro` steps into quantifiers and “eats” assumptions, if I see `constructor` I know it’s breaking apart the goal into multiple, and so on. Keep in mind that in reality all tactics do is aid you in producing a tree of terms. As in, actually the proofs are all tree-shaped. It’s even possible to write them that way directly. Tactics are more like a set of macros and DSL for writing that tree very concisely. So when I look at some tactics (constructor, use, refine, intro), I really see tree manipulation (“we’re splitting pieces, we’re filling in this part before that part, etc”). However, it’s still different from reading code in the sense that I’d need to click into the middle to know for sure what assertion a line is dealing with. How much this is a problem I’m not sure. In a well-written proof with a good idea, you can often retrace the shape of the argument by reading because the flow of thought is similar to a paper proof. So someone who wants to communicate what they’re doing is generally able to by choosing reasonable names, clear flow of the argument, appropriate tactics and — importantly! — extracting smaller lemmas for non-obvious results. Or even inline expressions that state hypotheses clearly before supplying a few lines of proof. On the other hand, there are cases where the proof is obvious to a human but the machine struggles and you have to write some boilerplate to grind through it. Those are sometimes solved by more powerful tactics, but sometimes you just have to write the whole thing. And in that case I don’t necessarily aim for it being “understandable” but for it being short. Lean users call that golfing. Golfed code has a specific flavor to it. Again in my experience golfing is used when a part of the proof would be obvious on paper (so a mathematician wouldn’t want to see 30 lines of code dedicated to that part), or when Lean itself is uniquely able to cut through some tedious argument. So to summarize, I feel like a lot of it is implicit, there are techniques to make it more explicit when the author wants, it doesn’t matter as much as I expected it would, and generally as your mental model of tactics improves, you’ll be able to read Lean code more fluidly without clicking. Also, often all you need to understand the argument is to overview the names of the lemmas it depends on. Whereas the specific order doesn’t matter because there’s a dozen way to restructure it without changing the substance.
bravesoul2 1y ago
I love the article. Few can cross the bridge and describe these sorts of things in an easy to digest way. The secret is showing all the tiny steps experts might not see as it is too obvious. Thank you!
- danabramov 1y ago
  Thanks!
Western0 1y ago
Better https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system Many books create, many proof
- fjfaase 1y ago
  I understand that the Mizar community is rather closed and primarily focused on extending the Mizar Mathematical Library. The Mizar proof checker is closed source. Lean is gaining traction, which can be seen from the fact that at the moment 81 [1] of the 100 theorems of the 'Formalizing 100 Theorems' [1] have been proven in Lean, while Mizar stands at 71 [3] [1] https://leanprover-community.github.io/100.html https://leanprover-community.github.io/100.html [2] https://www.cs.ru.nl/%7Efreek/100/ https://www.cs.ru.nl/%7Efreek/100/ [3] https://mizar.uwb.edu.pl/100/ https://mizar.uwb.edu.pl/100/
  - zozbot234 1y ago
    Mizar is actually available under a GPL 3 license (thus FLOSS) from https://github.com/MizarProject/system https://github.com/MizarProject/system . There's an experimental Rust reimplementation that's at least 5x faster than the original: https://github.com/digama0/mizar-rs https://github.com/digama0/mizar-rs
derdi 1y ago
Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.) I would find the following a more convincing presentation: theorem x_eq_x (x:nat) : x = x := by rfl theorem 2_eq_2 : 2 = 2 := by exact (x_eq_x 2) Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.
- danabramov 1y ago
  Fair! I decided not to do that because the way arguments work (and dependent types in general — like being able to return a proof of `x = x` given x) is unusual for people like me, and deserves an article of its own. So I’m kicking that to one of the next articles.
barrenko 1y ago
As an abstract rule of thumb, how much would one have to beef up on logic before attempting to screw around analysis and something like Lean?
- daxfohl 1y ago
  None at all. Hit the natural numbers game that was referenced and you can start proving basic things like 2+2=4, n+0=n on up to associativity, commutativity, etc of basic operations, etc.
  - barrenko 1y ago
    Appreciate it!
harperlee 1y ago
Perhaps this thread is a good place to ask, could anyone contribute their own opinion about the relative future of lean vs. idris/coq/agda? I want to dedicate some time to this from a knowledge representation point of view, but I'm unsure about which of them will have less risk of ending up as so many esoteric languages... I sank a lot of time on clojure core.logic for a related project and got burnt with the low interest / small community issue already, so I've been hesitant to start with any of them for some time.
- armchairhacker 1y ago
  IME Lean and Coq/Rocq are used more in practice, and have bigger libraries and communities, than Idris and Agda. Rocq is the most common for program verification, but I suspect mainly due to it being older, and it has weird quirks due to its age, so Lean may catch up. Lean is the most common for proving mathematical theorems. Big projects verified in Rocq include CompCert, CertiCoq, and sel4. Additionally, some large companies use Rocq to verify critical software like in airplanes (there's a list at https://github.com/ligurio/practical-fm https://github.com/ligurio/practical-fm although it may not be accurate). Big projects in Lean include mathlib (collection of various mathematical proofs), and the ongoing work to prove Fermat's Last Theorem (https://imperialcollegelondon.github.io/FLT/ https://imperialcollegelondon.github.io/FLT/) and PFR (https://teorth.github.io/pfr/ https://teorth.github.io/pfr/). I'm not aware of "real-world" projects in Idris and Agda but may be wrong. That said, they're all small communities compared to something like C++ or JavaScript. Moreover, verifying programs is very slow and tedious (relative to writing them), so I wouldn't be surprised if we see a big breakthrough (perhaps with AI) that fundamentally changes the landscape. But remember that even with a breakthrough your skills may be transferable.
- daxfohl 1y ago
  I wouldn't put much money on any of them. IME most mathematicians aren't that interested in formalization, and the gulf between a hand written proof and and a computer verified syntax is pretty huge. Theyre interesting to learn and play with for their own sake, but I'd be reluctant to make any bets on the future of any of them. If I had to choose, Lean seems to have the most momentum, though the others have been around longer and each has some loyal users.
77pt77 1y ago
Archive: https://web.archive.org/web/20250731115617/https://overreacted.io/the-math-is-haunted/ https://web.archive.org/web/20250731115617/https://overreact...
ninetyninenine 1y ago
I wonder if there’s any physical phenomena that can be modeled with inconsistent math. Like we assume everything is consistent but maybe it’s not.
- omnicognate 1y ago
  As the article explains (and the title alludes to), if your axioms are inconsistent, so you can prove a contradiction, you can prove anything. Literally any statement that can be formulated can be proven to be true (as can its negation!). So you'd be trying to model the universe with a maths in which 1 = 2. And also 1 = 3. And also 1 =/= 3. Any useful set of axioms has to be consistent, because any inconsistency is catastrophic. It wrecks the entire thing. Of course that also means, thanks to Godel's theorem, that any useful set of axioms is incomplete, in that there are true statements that cannot be proved from them.
  - ninetyninenine 1y ago
    I guess let me rephrase the question. Does there exist system that is inconsistent but the inconsistency is localized and therefore we can actually miss the inconsistency by not knowing or noticing the localized inconsistency? Is there a proof of what you said as well? An inconsistent system with the inconsistency in one spot can have any statement made about the system be both true and false? I’m adjusting the parameters here so we can ask the deeper question of whether one exists in the real world.
    - unexpectedtrap 1y ago
      “Paraconsistent logic” or “paraconsistent set theory” is what you are searching for.
      - ninetyninenine 1y ago
        I didn't think I'd get an answer to this, but awesome.
retr0rocket 1y ago
[dead]
retr0rocket 1y ago
[dead]
tonetheman 1y ago
[dead]

409 points by danabramov 1y ago

One problem I have with learning Lean is that tactics - like rfl in the example - are overloaded, and their full semantics not completely explained/understandable from the tutorials. Unlike, say, C programming where one may understand what happens to the program state down to the bit, it feels too fuzzy. And the rewrite (rw) tactic syntax doesn't feel natural either.

danabramov 1y ago
Yeah the documentation is also quite fragmented because tactics are user-definable and some are from Lean vs from Mathlib etc. I've gotten quite decent at using the basic ones but I still sometimes ask on Zulip if something isn't working as I expected.
LegionMammal978 1y ago
Yeah, I've similarly found the tactics in Coq (now Rocq) difficult to internalize. E.g., I might have "A = B" and "P(A,A)" available, and I want to conclude "P(A,B)", but the rewrite will fail for some arcane reason. (Issues with the definition of some of the intermediate structures, I'd imagine.) On the other end of the spectrum, I've recently been playing with Metamath and its set.mm database, which has no programmable tactics at all, only concrete inferences that can be used in a proof. (E.g., the modus ponens inference ax-mp says that "|- ph" and "|- ( ph -> ps )" prove "|- ps", where "ph" and "ps" are variables that can be substituted.) Alas, it's not much better, since now you have to memorize all the utility lemmas you might need!
- 7373737373 1y ago
  Agreed - the Metamath base language (and its verifier) seem to be the most tractable of all I've seen, although it is probably still quite far away from the complexity of the high level language(s) that compile to it. Derived from it, the currently best attempt to achieve an unambiguous and secure language seems to be Metamath Zero: https://github.com/digama0/mm0 https://github.com/digama0/mm0
solomonb 1y ago
This is why I prefer Agda, where everything comes down to pattern matching.
- agnishom 1y ago
  You can absolutely use pattern matching in Lean instead of tactics, if you prefer to write the proof that is closer to "what is going on under the hood"
  - solomonb 1y ago
    yeah i didn't mean to imply you cannot do that, but tactics seem to be highly encouraged. I'm actually a big fan of Lean, I just like it more as a programming language for writing programs with dependent types then as a proof checker.
gylterud 1y ago
This is one of the reasons I prefer Agda. It is usually written without tactics, you just write the proof term in a functional programming language via the Curry–Howard correspondence. The trade off is that you must be more disciplined with creating useful abstractions and functions, otherwise proving even routine stuff becomes really tedious.
- Paracompact 1y ago
  I'm not sure you prefer Agda so much as you prefer providing proof terms functionally rather than imperatively. Then again I've never used Agda; how does it differ from Coq/Rocq minus Ltac or Lean minus tactics?
  - logicchains 1y ago
    Coq has much less support for working with dependent types; you need lots of annotations compared to Agda (which has superior dependent pattern matching support). Lean is somewhere between the two.
kmill 1y ago
At least you can 'go to definition' on the tactics and see what they're doing. It's a lot to take in at the beginning, but it can all be inspected and understood. (At least until you get to the fundamental type theory; the reduction rules are a lot harder to get into.) > the rewrite (rw) tactic syntax doesn't feel natural either. Do you have any thoughts on what a natural rewrite syntax would be?
- 7373737373 1y ago
  > Do you have any thoughts on what a natural rewrite syntax would be? Not yet, but I'd probably prefer something that more explicitly indicated (in English, or some sort of more visually "pointing" indicator) which specific parts of the previous step would be replaced It feels weird, or I'd have to get used to that both what is being replaced and what it is replaced with depends on some distant context, it's very indirect as it requires switching attention between the tactics tree and the context or previous proofs
  - danabramov 1y ago
    If you have specific ideas, I'm also curious! I wonder if Lean can be extended to support what you're thinking of — its ability to have custom syntax and tactics seems really powerful. That's part of what excites me about Lean as I'm also not always the biggest fan of existing tactics, but they seem to evolve similarly to other pieces of software.
    - kmill 1y ago
      We're working on a new rewrite tactic this summer at the Lean FRO (I don't know if I ever directly mentioned that to you yet on Zulip). One interface I'm planning on is `rw [(pos := 1,3,2) thm]` to be able to navigate to the place where the rewrite should occur, with a widget interface to add these position strings by clicking on them in the Infoview. The whole occurrences interface will also be revamped, and maybe someone from the community could help make a widget interface for that too. Of course there's already `conv => enter [1,3,2]; rw thm`, but putting it directly into `rw` is more convenient while also being more powerful (`conv` has intrinsic limitations for which positions it can access). The interface is what people will notice, but technical idea of the project is to separate the "what" you want to rewrite from "how" to get dependent type theory to accept it, and then make the "how" backend really good at getting rewrites to go through. No more "motive not type correct", but either success or an error message that gives precise explanations of what went wrong with the rewrite. And, yeah, it's great that Lean lets you write your own tactics, since it lets people write domain-specific languages just for solving the sorts of things they run into themselves. There's no real difference between writing tactics as a user or as part of the Lean system itself. Anyone could make a new rewrite tactic as a user package.
swagmoney1606 1y ago
You may like Agda. I prefer Lean even though you are right about this.
emmelaich 1y ago
It was interesting to me as it didn't fit my expectations. As a math theory ignoramus, I expected that reflection and rewrite are more fundamental than addition. But Lean seems to assume addition but require explicit rfl and rewrite. Perhaps there's a Lean "prelude" that does it for you.
- derdi 1y ago
  Yes, there is a prelude that defines natural numbers and an addition function on them. As the post notes, the reflexivity tactic "unfolds" the addition, meaning that it applies the addition function to the constants it is given, to arrive at a constant. This is not specific to addition, it unfolds other function definitions too. So addition doesn't have to come first, you are right that reflexivity is more fundamental.
  - danabramov 1y ago
    Author here — this is correct. I’ve added a paragraph on this in an edit btw so it’s possible the parent poster hasn’t seen it yet. Reproducing the paragraph: (Here, rfl closes ⊢ 3 + 3 = 6, but for a different reason than one might think. It doesn’t really “know” that 3 + 3 is 6. Rather, rfl unfolds the definitions on both sides before comparing them. As 3, 6, and + get unfolded, both sides turn into something like Nat.zero.succ.succ.succ.succ.succ.succ. That’s why it actually is a something = something situation, and rfl is able to close it.) Also, another resource on this is https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/ https://xenaproject.wordpress.com/2019/05/21/equality-part-1...
    - emmelaich 1y ago
      Thanks! That makes sense.
- armchairhacker 1y ago
  It's because the addition can evaluate to only one form: `3 + 3` and `6` both evaluate to `succ (succ (succ (succ (succ (succ zero)))))`, similarly Lean can infer `4 * 3 = 1 + 3 + 8` because both evaluate to the same as `12`. But an expression can be rewritten to an infinite number of forms, e.g. `x * 2` can be rewritten to `x + x`, `(x + (x / 2)) * 4/3)`, etc. So `refl` can automatically evaluate both sides but not rewrite them.
gowld 1y ago
One thing Lean inherits from mathematics is the use of opaque notation. It would be nice to inherit some readability from programming. Paperproof is an effort in one direction (visualization of the logic tree) https://paperproof.brick.do/lean-coq-isabel-and-their-proof-trees-yjnd2O2RgxwV https://paperproof.brick.do/lean-coq-isabel-and-their-proof-...
daxfohl 1y ago
The surprising thing to me was that tactics are all written in "user-level" code, outside the proof kernel. This makes sense in the sense that you want a small, thoroughly tested kernel that doesn't change. But it also implies that if you use tactics in your proof, then your proof can go from correct to failing if one of the tactics you use gets modified between releases. Is that a problem in real world use?
- Tainnor 1y ago
  Yes. I've seen proofs fail after a mathlib update because the behaviour of simp changed. I've never seen it do less after an update (so far), but sometimes it'll simplify more and then the next steps may fail to work. I've since adopted the suggestion (that is afaik used in mathlib) to never use bare simp unless it closes the current goal directly. Instead, if you write simp?, Lean will run the simplifier and tell you exactly which theorems it used (in the form of simp only [...]) which you can then insert into the proof instead.
  - daxfohl 1y ago
    I guess it makes sense: the tactics are defined in the lean repo (but not in the kernel of that repo), while mathlib has its own repo. But any changes to tactic code triggers a test to verify that mathlib still works against it. Which implies there's a reasonable set of checks and balances that don't allow tactic changes to break anything too badly if you follow mathlib's idioms, though it can still happen.
Tainnor 1y ago
I understand what you mean, but I shudder to think at how complicated it would be to write certain proofs without tactics, e.g. simp, ring, omega, linarith and friends all really do a lot of work.

kevinqi 1y ago

as someone who hasn't seen Lean before but was curious from alphaproof, love the intro! curious if you can mention what you're working on in Lean?

danabramov 1y ago
For now I'm just learning math with it! Currently I'm going through https://github.com/teorth/analysis https://github.com/teorth/analysis (Tao's Lean companion to his textbook) and filling in the `sorry`s in the exercises (my solutions are in https://github.com/gaearon/analysis-solutions https://github.com/gaearon/analysis-solutions).
- kevinqi 1y ago
  very cool. btw, I also love that "sorry" is the "any" equivalent in Lean

7373737373 1y ago

Does Lean have some sort of verification mode for untrusted proofs that guarantees that a given proof certainly does not use any "sorry" (however indirectly), and does not add to the "proving power" of some separately given fixed set of axioms with further axioms or definitions?

jonny_eh 1y ago
Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355 https://github.com/leanprover/lean3/issues/1355
- kmill 1y ago
  That's Lean 3, from eight years ago, and it's from before 'sorry' really existed in the way we know it now. --- To answer the GP's question: Not only is there a verification mode, but Lean generates object files with the fully elaborated definitions and theorems. These can be rechecked by the kernel, or by external verifiers. There's no need to trust the Lean system itself, except to make sure that the theorem statements actually correspond to what we think they're supposed to be.
  - treyd 1y ago
    What exactly do these object files look like?
    - kmill 1y ago
      The "olean" files are a binary format that contain everything that was added to the Lean environment. Among other things, it includes all of the declarations and their Lean.Expr [1] expressions. People have written tools to dump the data for inspection [2], or to independently check that the expressions are type correct and the environment is well-formed (that is, check the correctness). [1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd454711e2f9e4e20cbbde47ba85/src/Lean/Expr.lean#L302 https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib

deleted 1y ago

[deleted]

cubefox 1y ago

One thing I didn't know until recently was that Lean doesn't solve the problem of verifying that a formal theorem actually states what we think it states rather than something else. In some cases that's not an issue, because the formal statement of the theorem is very simple. E.g. for Fermat's Last Theorem, which can be formally expressed with "(x y z : ℕ+) (n : ℕ) (hn : n > 2) : x^n + y^n ≠ z^n". But in other cases it might be much harder to verify that a formal statement actually matches the intuitive informal statement we want. Of course, Lean or similar languages still offer the huge potential of verifying that a formal statement is provable, even if they don't help with verifying that the formal statement matches the intended informal statement in natural language.

danabramov 1y ago
Are there, in general, ways to do that? Sorry if this sounds like a troll question, but I struggle to think of how one would verify that a formal statement matches the accepted understanding other than painstakingly going through the definitions with experts from both sides.
- cubefox 1y ago
  I don't think there is any technical solution for that, apart perhaps from asking an LLM, or multiple different LLMs, whether it thinks the formal definition matches the informal statement. When mathematicians check normal (informal) proofs they usually verify both things at once: that the proof doesn't contain mistakes or insufficiencies, and that it proves what the author says it proves. Formal proof checkers aren't able to do the latter.
  - danabramov 1y ago
    I personally view proof checkers as mathematicians' tools so I assume mathematicians would be involved either way. With some percentage actually preferring to work closely with these tools. See also Terence Tao's comment in https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/#comment-688326 https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t... which feels relevant to me

brookst 1y ago

I’ve been kicking around the idea of something like Lean (maybe even just Lean?) to rewrite news and other non-fiction articles, treating statements as theorems that need to be proven. Proofs could include citations, and could be compound things like “this is a fact if three of my approved sources asserted it as a fact” It should then be possible to get a marked-up version of any document with highlighting for “proven” claims. Sure, it’s not perfect, but I think it would be an interesting way to apply the rigor that used to be the job of publications.

ants_everywhere 1y ago
I don't know why you're getting downvoted because I think this is an interesting idea. Completely impossible but still interesting and fun to explore. But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples
- ramses0 1y ago
  Basically [Citation Needed]
- almostgotcaught 1y ago
  [flagged]
  - riku_iki 1y ago
    But such system exists, mostly implemented in prolog.
    - ants_everywhere 1y ago
      Does it actually?
      - kevindamm 1y ago
        The first thing this thread made me think of: https://cyc.com/ https://cyc.com/ It's been around for decades.. I'm sure there are other similar systems.

Waterluvian 1y ago

Wait… so are we basically compiling a dictionary of proofs all stemming from a handful of self-evident truths? And every further proof is just some logical aggregation of previous proofs? Can someone please turn this into a Zachtronics style game?! I badly, direly want this. There’s a game called Euclidea that’s kind of like this for trigonometry and the whole premise of building a tower of logic is deeply attractive to me. Is this what pure math is about? Is this what people who become math profs are feeling in their soul? The sheer thrill of adding to that dictionary of proofs? Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.

danabramov 1y ago
Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.
hobs 1y ago
You probably are vaguely referencing the Principa Mathematica.
- Tainnor 1y ago
  That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.
treyd 1y ago
You might be thinking of Euclid's axioms, which defines points, lines, planes, etc, and that lines can be parallel. This is an interesting one because the system is violated if your space is not flat, like if you're on a sphere. You could also be thinking of Zermelo-Fraenknel set theory (ZF/ZFC), which most of modern mathematics is ultimately based upon.
- deleted 1y ago
  [deleted]

andoando 1y ago

Is there a standard library/repository of all existing mathematical proofs one can add to?

ants_everywhere 1y ago
There are a few. The lean one is at https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4

DoctorOetker 1y ago

I possess a proof of FLT, and will publish the metamath formalization, in due time (first I need to build a secure display, for reasons that will become clear).

olddustytrail 1y ago
Fermat's Last Theorem is easily solved with css. Just do: margin-left: 200px; and you're sorted.
- DoctorOetker 1y ago
  people jest, but they will jest less once they think a little more critically: how can cryptography experts expound the security of such and such cryptographic primitives involving discrete numbers, exponentiation, ... but be unable to come up with alternative proofs of FLT? ... but be unable to individually formalize existing supposed proof of FLT? ... but be unable to find a more succinct proof of FLT? who knows their way around the block, if the consensus is that Fermat did not possess a proof but Wiles did finally find a proof, who knows their way around the block, if a much more succinct proof than Wiles long-winded-anc-to-this-date-not-formally-verified-proof? would you jest less?
  - olddustytrail 1y ago
    I probably wouldn't. I'm in a jovial mood and I've managed to joke about many of the worst parts of my life. There are many worse things happening in the world than issues in mathematics. You seem in a serious mood but these things too shall pass.
    - DoctorOetker 1y ago
      > There are many worse things happening in the world than issues in mathematics. But mathematics in general and cryptography in specific, and the canon / propaganda that surrounds it is intimately affecting the principal variation of the same events you so lament.
  - 1y ago

nowittyusername 1y ago

I wonder suppose you are not relying on any tricks or funky shenanigans. is it possible to just throw random stuff at Lean and find interesting observations based if it approves? like use an automated system or an llm that tries all types of wild proofs/theories? and sees if it works? maybe im asking wrong questions though or not stating it well.. this is above my understanding, i could barely get my head around prolog.

Paracompact 1y ago
As someone who does certified programming professionally, I believe generative AI and formal methods are a match made in heaven. I might even go so far as to wager that the notion that human programmers will or will not be replaced by LLM-based AI is entirely dependent on whether these AI can get good at certified programming + compositional reasoning. > is it possible to just throw random stuff at Lean and find interesting observations based if it approves? Traditional AI has an easy time with checkers, because the search space is small. Chess is a little harder. Go still cannot be reasonably tackled by non-machine learning AI. Meanwhile, the search space (number of available moves together with the diversity of explorable states) for a sophisticated formal language becomes unfathomably large. When the problem is known to be of a certain nature, often you can time-efficiently brute force it via SMT solvers. Traditionally SMT solvers and proof assistants have been separate branches of formal methods, but they're finally learning to play off each other's strengths (cf. Sledgehammer, Lean-SMT). > like use an automated system or an llm that tries all types of wild proofs/theories? and sees if it works? Research in this vein needs to be made more mainstream. I'm excited, though, that there have been big funders behind these ideas for years now, even before LLMs became big. Cf. "Learning to Find Proofs and Theorems by Learning to Refine Search Strategies" for earlier work, or DeepSeek-Prover for more recent attempts. I'm no machine learning expert, but it seems it's still a very open question how to best train these things and what their future potential is. All in all mainstream LLMs are still rather mediocre at languages like Rocq and Lean. And when they're wrong, their proof scripts are extremely tedious to try to troubleshoot and correct. But I have hope AI tooling in formal methods will mature greatly over time.
- benreesman 1y ago

thresholds 1y ago

Paging Terrence Howard

ljlolel 1y ago

Maybe before we have AGI we should get an AI that can translate Andrew’s proof into Lean for us. Easily tractable, checkable, useful, and build-upon-able

grumbelbart2 1y ago
Work is already underway in that direction: https://github.com/deepseek-ai/DeepSeek-Prover-V2 https://github.com/deepseek-ai/DeepSeek-Prover-V2 but also https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/ https://deepmind.google/discover/blog/alphaevolve-a-gemini-p... Terence Tao is doing a lot of work in this direction.
zozbot234 1y ago
Kevin Buzzard is reportedly working on formalizing a modern proof of FLT. This effort has already managed to surface some unsound arguments in one of the prereqs for the proof (namely crystalline cohomology) https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ https://xenaproject.wordpress.com/2024/12/11/fermats-last-th... though the issue has since been fixed.

Karliss 1y ago

Is there a way to read lean proofs noninteractively. After playing with the natural number a game a bit, proofs quickly ended up being opaque sequences of "rw [x]" commands which felt unreadable. It's nice that the editor allows interactively viewing the state at different points, but having to click on each line ruins the flow of reading. Imagine if you had to read python code which has no indentation, braces or anything similar and only way to know where if statement ends or an else block starts is by clicking on each line. My impression might be influenced by the limited vocabulary that the early levels of natural number game provides. Does the richer toolset provided by full lean make it easier to make proofs readable without requiring you to click on each line to get the necessary context?

RossBencina 1y ago
> Is there a way to read lean proofs noninteractively. I'd like to see an answer to this question. I was looking into it the other day. I found this: https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ Which gives a way to do the clicking-through outside the editor. And maybe gives some insight into how Lean people see things.
danabramov 1y ago
This is a great question! I’m still not very experienced so take it with a grain of salt. But here’s my take on it. I’ve been spending time with Lean quite a bit for the past few months. When I look at a proof, I don’t “read” it the same way as I do with programming. It feels a bit more like “scanning”. What stands out is the overall structure of the argument, what tactics are used, and what lemmas are used. In real Lean code, the accepted style is to indent any new goals, work on one goal at a time (except a few special parallel tactics), and outdent when the goal is done. That’s what I mean by the “shape” of the argument. See some examples in this PR I’m working on: https://github.com/gaearon/analysis-solutions/pull/7/files https://github.com/gaearon/analysis-solutions/pull/7/files Once you’re familiar with what tactics do, you can infer a lot more. For example `intro` steps into quantifiers and “eats” assumptions, if I see `constructor` I know it’s breaking apart the goal into multiple, and so on. Keep in mind that in reality all tactics do is aid you in producing a tree of terms. As in, actually the proofs are all tree-shaped. It’s even possible to write them that way directly. Tactics are more like a set of macros and DSL for writing that tree very concisely. So when I look at some tactics (constructor, use, refine, intro), I really see tree manipulation (“we’re splitting pieces, we’re filling in this part before that part, etc”). However, it’s still different from reading code in the sense that I’d need to click into the middle to know for sure what assertion a line is dealing with. How much this is a problem I’m not sure. In a well-written proof with a good idea, you can often retrace the shape of the argument by reading because the flow of thought is similar to a paper proof. So someone who wants to communicate what they’re doing is generally able to by choosing reasonable names, clear flow of the argument, appropriate tactics and — importantly! — extracting smaller lemmas for non-obvious results. Or even inline expressions that state hypotheses clearly before supplying a few lines of proof. On the other hand, there are cases where the proof is obvious to a human but the machine struggles and you have to write some boilerplate to grind through it. Those are sometimes solved by more powerful tactics, but sometimes you just have to write the whole thing. And in that case I don’t necessarily aim for it being “understandable” but for it being short. Lean users call that golfing. Golfed code has a specific flavor to it. Again in my experience golfing is used when a part of the proof would be obvious on paper (so a mathematician wouldn’t want to see 30 lines of code dedicated to that part), or when Lean itself is uniquely able to cut through some tedious argument. So to summarize, I feel like a lot of it is implicit, there are techniques to make it more explicit when the author wants, it doesn’t matter as much as I expected it would, and generally as your mental model of tactics improves, you’ll be able to read Lean code more fluidly without clicking. Also, often all you need to understand the argument is to overview the names of the lemmas it depends on. Whereas the specific order doesn’t matter because there’s a dozen way to restructure it without changing the substance.

bravesoul2 1y ago

I love the article. Few can cross the bridge and describe these sorts of things in an easy to digest way. The secret is showing all the tiny steps experts might not see as it is too obvious. Thank you!

danabramov 1y ago
Thanks!

Western0 1y ago

Better https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system Many books create, many proof

fjfaase 1y ago
I understand that the Mizar community is rather closed and primarily focused on extending the Mizar Mathematical Library. The Mizar proof checker is closed source. Lean is gaining traction, which can be seen from the fact that at the moment 81 [1] of the 100 theorems of the 'Formalizing 100 Theorems' [1] have been proven in Lean, while Mizar stands at 71 [3] [1] https://leanprover-community.github.io/100.html https://leanprover-community.github.io/100.html [2] https://www.cs.ru.nl/%7Efreek/100/ https://www.cs.ru.nl/%7Efreek/100/ [3] https://mizar.uwb.edu.pl/100/ https://mizar.uwb.edu.pl/100/
- zozbot234 1y ago
  Mizar is actually available under a GPL 3 license (thus FLOSS) from https://github.com/MizarProject/system https://github.com/MizarProject/system . There's an experimental Rust reimplementation that's at least 5x faster than the original: https://github.com/digama0/mizar-rs https://github.com/digama0/mizar-rs

derdi 1y ago

Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.) I would find the following a more convincing presentation: theorem x_eq_x (x:nat) : x = x := by rfl theorem 2_eq_2 : 2 = 2 := by exact (x_eq_x 2) Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.

danabramov 1y ago
Fair! I decided not to do that because the way arguments work (and dependent types in general — like being able to return a proof of `x = x` given x) is unusual for people like me, and deserves an article of its own. So I’m kicking that to one of the next articles.

barrenko 1y ago

As an abstract rule of thumb, how much would one have to beef up on logic before attempting to screw around analysis and something like Lean?

daxfohl 1y ago
None at all. Hit the natural numbers game that was referenced and you can start proving basic things like 2+2=4, n+0=n on up to associativity, commutativity, etc of basic operations, etc.
- barrenko 1y ago
  Appreciate it!

harperlee 1y ago

Perhaps this thread is a good place to ask, could anyone contribute their own opinion about the relative future of lean vs. idris/coq/agda? I want to dedicate some time to this from a knowledge representation point of view, but I'm unsure about which of them will have less risk of ending up as so many esoteric languages... I sank a lot of time on clojure core.logic for a related project and got burnt with the low interest / small community issue already, so I've been hesitant to start with any of them for some time.

armchairhacker 1y ago
IME Lean and Coq/Rocq are used more in practice, and have bigger libraries and communities, than Idris and Agda. Rocq is the most common for program verification, but I suspect mainly due to it being older, and it has weird quirks due to its age, so Lean may catch up. Lean is the most common for proving mathematical theorems. Big projects verified in Rocq include CompCert, CertiCoq, and sel4. Additionally, some large companies use Rocq to verify critical software like in airplanes (there's a list at https://github.com/ligurio/practical-fm https://github.com/ligurio/practical-fm although it may not be accurate). Big projects in Lean include mathlib (collection of various mathematical proofs), and the ongoing work to prove Fermat's Last Theorem (https://imperialcollegelondon.github.io/FLT/ https://imperialcollegelondon.github.io/FLT/) and PFR (https://teorth.github.io/pfr/ https://teorth.github.io/pfr/). I'm not aware of "real-world" projects in Idris and Agda but may be wrong. That said, they're all small communities compared to something like C++ or JavaScript. Moreover, verifying programs is very slow and tedious (relative to writing them), so I wouldn't be surprised if we see a big breakthrough (perhaps with AI) that fundamentally changes the landscape. But remember that even with a breakthrough your skills may be transferable.
daxfohl 1y ago
I wouldn't put much money on any of them. IME most mathematicians aren't that interested in formalization, and the gulf between a hand written proof and and a computer verified syntax is pretty huge. Theyre interesting to learn and play with for their own sake, but I'd be reluctant to make any bets on the future of any of them. If I had to choose, Lean seems to have the most momentum, though the others have been around longer and each has some loyal users.

77pt77 1y ago

Archive: https://web.archive.org/web/20250731115617/https://overreacted.io/the-math-is-haunted/ https://web.archive.org/web/20250731115617/https://overreact...

ninetyninenine 1y ago

I wonder if there’s any physical phenomena that can be modeled with inconsistent math. Like we assume everything is consistent but maybe it’s not.

omnicognate 1y ago
As the article explains (and the title alludes to), if your axioms are inconsistent, so you can prove a contradiction, you can prove anything. Literally any statement that can be formulated can be proven to be true (as can its negation!). So you'd be trying to model the universe with a maths in which 1 = 2. And also 1 = 3. And also 1 =/= 3. Any useful set of axioms has to be consistent, because any inconsistency is catastrophic. It wrecks the entire thing. Of course that also means, thanks to Godel's theorem, that any useful set of axioms is incomplete, in that there are true statements that cannot be proved from them.
- ninetyninenine 1y ago
  I guess let me rephrase the question. Does there exist system that is inconsistent but the inconsistency is localized and therefore we can actually miss the inconsistency by not knowing or noticing the localized inconsistency? Is there a proof of what you said as well? An inconsistent system with the inconsistency in one spot can have any statement made about the system be both true and false? I’m adjusting the parameters here so we can ask the deeper question of whether one exists in the real world.
  - unexpectedtrap 1y ago
    “Paraconsistent logic” or “paraconsistent set theory” is what you are searching for.
    - ninetyninenine 1y ago
      I didn't think I'd get an answer to this, but awesome.

retr0rocket 1y ago

[dead]

retr0rocket 1y ago

[dead]

tonetheman 1y ago

[dead]