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.
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?
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.
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?
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.
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?
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.
>Lean doesn't solve the problem of verifying that a formal theorem actually states what we think it states rather than something else.
With all honesty, if a tool existed that did that we would have solved maths. Or at least we would have solved human communication. In both cases it would be the most studied thing in the world, so I don't know where this belief would come from
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.
Check out https://argdown.org/ for the much simpler version of that idea. No proofs, just supporting/conflicting evidence and arguments. But that's hard enough to consistently produce as it is.
I think you could just use lean, and progressively elaborate the inference graph.
But you might find a historical/journalistic/investigative angle more profitable.
I heard a software product pitch from a small law practice who were outside investigators for abuse/policy-violation claims in a unionized workforce. They had a solid procedure: start with the main event. Interview all witnesses, and identify other interesting events. Then cross-reference all witnesses against all alleged/interesting events. That gives you a full matrix to identify who is a reliable witness, what sort of motivations are in play, and what stories are being told, patterns of behaviour, etc. Their final report might actually focus on another event entirely that had better evidence around it.
In that sort of historical investigation, a single obviously false claim undermines all claims from that witness. Pure logic doesn't have that bi-directionality of inference. Sometimes your sources just flat out lie! That's half the work.
The key difference is between a full matrix of claims vs sources/evidence, while good math is all about carefully plotting a sparse inference graph that traverses the space. What is called "penetrating minimalism" in math is called "cherry picking" in history or journalism.
We passed on the pitch. Didn't see how it scaled to a product worth building, but their process was appealing. Much better than the an internal popularity-contest or witch-hunt. Probably better than the average police investigation too.
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.
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).
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.
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
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?
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!
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.
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.
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.
33 comments
[ 2.3 ms ] story [ 48.3 ms ] thread> the rewrite (rw) tactic syntax doesn't feel natural either.
Do you have any thoughts on what a natural rewrite syntax would be?
Perhaps there's a Lean "prelude" that does it for you.
Paperproof is an effort in one direction (visualization of the logic tree)
https://paperproof.brick.do/lean-coq-isabel-and-their-proof-...
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.
With all honesty, if a tool existed that did that we would have solved maths. Or at least we would have solved human communication. In both cases it would be the most studied thing in the world, so I don't know where this belief would come from
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.
But you might find a historical/journalistic/investigative angle more profitable.
I heard a software product pitch from a small law practice who were outside investigators for abuse/policy-violation claims in a unionized workforce. They had a solid procedure: start with the main event. Interview all witnesses, and identify other interesting events. Then cross-reference all witnesses against all alleged/interesting events. That gives you a full matrix to identify who is a reliable witness, what sort of motivations are in play, and what stories are being told, patterns of behaviour, etc. Their final report might actually focus on another event entirely that had better evidence around it.
In that sort of historical investigation, a single obviously false claim undermines all claims from that witness. Pure logic doesn't have that bi-directionality of inference. Sometimes your sources just flat out lie! That's half the work.
The key difference is between a full matrix of claims vs sources/evidence, while good math is all about carefully plotting a sparse inference graph that traverses the space. What is called "penetrating minimalism" in math is called "cherry picking" in history or journalism.
We passed on the pitch. Didn't see how it scaled to a product worth building, but their process was appealing. Much better than the an internal popularity-contest or witch-hunt. Probably better than the average police investigation too.
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.
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?
I would find the following a more convincing presentation:
Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.https://web.archive.org/web/20250731115617/https://overreact...
Like we assume everything is consistent but maybe it’s not.
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.