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.
magicalhippo · 46m 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.
I found I got much better at writing non-fiction after having math at uni. I would help proof-read essays and other hand-ins by my SO and sister, and apply similar rigor as you mention. Stuff like "you show C follows from B here, but you haven't actually given an argument for why B follows A, so you can't then claim C follows from A".
It's tempting to say that with LLMs this seems like a plausible task to turn it into a program, but the hallucination issue puts a damper on that scheme.
No comments yet
bjackman · 29m ago
I think it's quite rare that the most important beliefs you should derive from the news can be justified by a collection of absolute statements.
I think you'd be better served by a tool for calculating chains of Bayesian reasoning. I've seen a tool that does this for numerical estimations.
ants_everywhere · 4h 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 · 4h ago
Basically [Citation Needed]
almostgotcaught · 3h ago
> I don't know why you're getting downvoted because I think this is an interesting idea
Because it's a completely gibberish idea along the lines I've of "I've been kicking around the idea of making pigs fly". Like kick around all you want but it ain't gonna happen.
ants_everywhere · 2h ago
Argument mining and automatic fact checking are things and there are actual products that do them.
It seems reasonable to have some of those products implemented in a logic language.
im3w1l · 1h ago
I think a logic language is not a great fit, because it deals in absolute truths. Whereas news and non-fiction articles are more someone said something and they are usually reliable except in this particular domain where they can be a bit biased sometimes. Also the people they interviewed may have misremembered. Etc etc.
You could argue that all such things could in principle be modelled in logical formulas but... it would be way more complicated than the stated model.
On the other hand it's also unclear what the logical model actually adds. Usually logical formulas are used because they can be manipulated, and inferences can be drawn. But drawing logical inferences from sorta-kinda true statements can quickly become muddy and lead to false conclusions if you don't take into account the uncertainty of the statements.
poeticsilence · 32m ago
Plenty of logics with non-binary truth values...
riku_iki · 3h ago
But such system exists, mostly implemented in prolog.
ants_everywhere · 2h ago
Does it actually?
adastra22 · 33m ago
There are many variations, but I’m on mobile rn. (Is this the new Fermat’s last theorem?)
But seriously, the idea of breaking claims into logic and using programming languages to check, compose, and verify claims is kinda the reason logical programming languages like prolog were invented.
It's been around for decades.. I'm sure there are other similar systems.
ljlolel · 5m 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
Waterluvian · 5h 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.
wging · 3h ago
There is a game already, though it may not be exactly what you want (and the goal is definitely not "generate all known math"). I've played around with it, and I do think it's pretty fun.
Had a blast with that game, really scratched that puzzle itch, and got to relearn some long-forgotten knowledge.
Waterluvian · 2h ago
How did I miss this! Thanks for pointing it out. This is scratching the itch.
treyd · 5h 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.
No comments yet
ants_everywhere · 5h ago
> Can someone please turn this into a Zachtronics style game?!
That game is called math :) Partially joking, but I do think a game version would be fun.
> Is this what pure math is about?
More or less yes for an undergrad, but when you get to research it feels different.
> I badly, direly want this
Consider checking out an abstract algebra book. Maybe Dummit and Foote or something else popular. Proofs in algebra often have a satisfying game-like quality. The more popular books will have solutions you can find online if you get stuck.
danabramov · 3h ago
>More or less yes for an undergrad, but when you get to research it feels different.
Would you mind telling more about how it feels different in research?
ants_everywhere · 2h ago
You can get into a meditative zone when you're manipulating equations using techniques you've internalized.
In research you're doing a lot more of things like reading papers, putting your thoughts into words, trying to understand something the author of the paper barely understands, feeling lost and unsure where to look next. All of that can feel good too (or it cannot depending on the person) but it's a different feeling than playing a logic game.
As one example, Euclidia is a fun meditative game. But compare the difference in feeling between doing an exercise from Euclid and trying to prove the parallel postulate. It took centuries to realize you couldn't prove it, and then there was a lot of hard work trying to figure out what geometry was like if you get rid of it.
jheitmann · 3h ago
Check out the game Bombe [1]. It's a minesweeper variant where instead of directly flagging or uncovering cells, you define rules for when cells can be flagged. As it gets more advanced you end up building lemmas that implicitly chain off each other. Then as _you_ get more advanced (and the game removes some arbitrary restrictions around your toolset) you can generalize your rules and golf down what you've already constructed.
Some good mentions elsewhere in the thread, another to check out is The Incredible Proof Machine https://incredible.pm/
swagmoney1606 · 4h ago
In my mind this is literally what math is. We start with axioms, and derive conclusions. There's probably more to it than that, but that's the understanding I'm at now.
JonChesterfield · 3h ago
Choosing the axioms is difficult.
danabramov · 4h ago
Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.
hobs · 5h ago
You probably are vaguely referencing the Principa Mathematica.
7373737373 · 7h 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.
LegionMammal978 · 7h 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 · 6h 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
gylterud · 6h 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.
emmelaich · 1h 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.
kmill · 5h 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 · 5h 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 · 3h 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.
solomonb · 6h ago
This is why I prefer Agda, where everything comes down to pattern matching.
agnishom · 3h 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"
swagmoney1606 · 4h ago
You may like Agda. I prefer Lean even though you are right about this.
danabramov · 7h 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.
nowittyusername · 2h 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.
kevinqi · 7h 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?
very cool. btw, I also love that "sorry" is the "any" equivalent in Lean
7373737373 · 7h 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?
danabramov · 7h ago
Does `#print axioms some_theorem` mentioned at the end of the article qualify? This would show if it depends on `sorry`, even transitively, or on some axioms you haven't vetted.
7373737373 · 7h ago
Oh, I missed that, thanks! It would be cool to use this to visualize the current state and progress on, and depth of the "proof dependency graph"!
masterjack · 7h ago
Yes, you can `print axioms` to make sure no axioms were added, make sure it compiles with no warnings or errors. There’s also a SafeVerify utility that checks more thoroughly and catches some tricks that RL systems have found
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 · 5h ago
What exactly do these object files look like?
kmill · 5h 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).
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).
andoando · 5h ago
Is there a standard library/repository of all existing mathematical proofs one can add to?
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 · 6h 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.
adastra22 · 26m ago
Yeah, by adopting Lojban as our common language.
Joking of course, but only because Lojban doesn’t have formally specified semantics.
Computational semantics could, in principle, allow you to enumerate the possible logical meanings of a given informal English phrasing of the statement, and these can be either each proven or thrown out with explicit justification for why that was not what you meant.
tunesmith · 5h ago
Yeah this seems like the specification/implementation problem. One can perfectly implement a bad spec, but coming up with the perfect spec is a human problem.
cubefox · 5h 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 · 3h 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-t... which feels relevant to me
cubefox · 2h ago
Tao misunderstands the question here: it was about reconciling a traditional (informal) proof and a formal proof which come to opposite conclusions, not about two different formal proofs.
danabramov · 1h ago
I think he accounts for that in the answer, "in a way that would be faster than if one or both proofs were informal" (which assumes "one formal and one informal" is also a case he's talking about). The way I understand his point is that in either case you would have to go through the two mathematical structures with the same amount of rigour and attention until you find the divergence, and that's easier to do when at least one side is formal (but can be done in either case).
In other words, informal math doesn't make this problem easier because you can still make and miss mistakes in encoding intent into the structure. But at least with formal math, there's whole classes of mistakes that you can't make.
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.
I found I got much better at writing non-fiction after having math at uni. I would help proof-read essays and other hand-ins by my SO and sister, and apply similar rigor as you mention. Stuff like "you show C follows from B here, but you haven't actually given an argument for why B follows A, so you can't then claim C follows from A".
It's tempting to say that with LLMs this seems like a plausible task to turn it into a program, but the hallucination issue puts a damper on that scheme.
No comments yet
I think you'd be better served by a tool for calculating chains of Bayesian reasoning. I've seen a tool that does this for numerical estimations.
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
Because it's a completely gibberish idea along the lines I've of "I've been kicking around the idea of making pigs fly". Like kick around all you want but it ain't gonna happen.
It seems reasonable to have some of those products implemented in a logic language.
You could argue that all such things could in principle be modelled in logical formulas but... it would be way more complicated than the stated model.
On the other hand it's also unclear what the logical model actually adds. Usually logical formulas are used because they can be manipulated, and inferences can be drawn. But drawing logical inferences from sorta-kinda true statements can quickly become muddy and lead to false conclusions if you don't take into account the uncertainty of the statements.
But seriously, the idea of breaking claims into logic and using programming languages to check, compose, and verify claims is kinda the reason logical programming languages like prolog were invented.
https://cyc.com/
It's been around for decades.. I'm sure there are other similar systems.
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.
The article mentions it, in fact: https://adam.math.hhu.de/#/g/leanprover-community/nng4
You could also be thinking of Zermelo-Fraenknel set theory (ZF/ZFC), which most of modern mathematics is ultimately based upon.
No comments yet
That game is called math :) Partially joking, but I do think a game version would be fun.
> Is this what pure math is about?
More or less yes for an undergrad, but when you get to research it feels different.
> I badly, direly want this
Consider checking out an abstract algebra book. Maybe Dummit and Foote or something else popular. Proofs in algebra often have a satisfying game-like quality. The more popular books will have solutions you can find online if you get stuck.
Would you mind telling more about how it feels different in research?
In research you're doing a lot more of things like reading papers, putting your thoughts into words, trying to understand something the author of the paper barely understands, feeling lost and unsure where to look next. All of that can feel good too (or it cannot depending on the person) but it's a different feeling than playing a logic game.
As one example, Euclidia is a fun meditative game. But compare the difference in feeling between doing an exercise from Euclid and trying to prove the parallel postulate. It took centuries to realize you couldn't prove it, and then there was a lot of hard work trying to figure out what geometry was like if you get rid of it.
[1] https://steamcommunity.com/app/2262930
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!
Derived from it, the currently best attempt to achieve an unambiguous and secure language seems to be Metamath Zero: https://github.com/digama0/mm0
Perhaps there's a Lean "prelude" that does it for you.
> the rewrite (rw) tactic syntax doesn't feel natural either.
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
Currently I'm going through 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).
---
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.
[1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib
The lean one is at https://github.com/leanprover-community/mathlib4
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.
Joking of course, but only because Lojban doesn’t have formally specified semantics.
Computational semantics could, in principle, allow you to enumerate the possible logical meanings of a given informal English phrasing of the statement, and these can be either each proven or thrown out with explicit justification for why that was not what you meant.
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.
In other words, informal math doesn't make this problem easier because you can still make and miss mistakes in encoding intent into the structure. But at least with formal math, there's whole classes of mistakes that you can't make.