Formalising natural language statements is a minefield of difficulties, for (imo) essentially the same reasons that writing code which interacts with the real world is so difficult. Concepts you take for granted like identity, time, causality... all of that stuff needs to be fleshed out carefully and precisely in the formalism for facts to be relatable to each other (or even expressible in the first place).

Not to discourage you - it's a cool problem! OpenCog comes to mind as a project that tried to take this all the way, and there's a field devoted to this stuff in academia called KRR (knowledge representation and reasoning). The IJCAI journal is full of research on similar topics.

(also see all the different logics philosophers use to formalise different kinds of argument involving time/modality/probability - there are a lot, but they aren't very "modular" and can't easily be mixed unless someone has solved that since I last looked into it)

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.

> 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.

Careful, such an approach could easily end up giving an aura of logical objectivity to arbitrarily radical and nonsensical ideas. The political views of one of the fathers of modern logic may serve as a cautionary tale [0].

[0] https://en.m.wikipedia.org/wiki/Gottlob_Frege#Political_view...

I think it'd be more interesting to map out entire trees of arguments about a topic. Start with something big, like "is there a God," then come up with all of the arguments for or against, then come up with all of the arguments against those arguments, then the counters to those arguments. Really explore it as a sort of debate space. Then bring in citations not as backing but for historical context: "Plato made this argument in such and such." The idea wouldn't be so much to decide a winner as to prevent us from going around in circles by making a map.

Proof != evidence. In evidence, we corroborate, collate, add more sources, weigh evidence, judge. Proof is a totally different process. Only in the mathematical do one prove something, everywhere else we build up evidence, corroborate, etc.

News and non-fiction articles are not math and cannot be treated as math. At best you could build a tool that check the most glaring contradictions (like a typo changing a number), and I'm not even sure it can be consistent without building a software that understand language. At worse you would build a tool that spit bullshit that millions of people would treat as gospel

For the form, you might be interested in Ethica, by Spinoza [1]. On the other hand, for fact checking, the key concept seems to be trust in sources rather than logical consistency.

[1]: https://en.wikipedia.org/wiki/Spinoza%27s_Ethics

This might be interesting to you: https://en.m.wikipedia.org/wiki/Stephen_Toulmin#The_Toulmin_...

Claimify from MS research aims in this direction. There's a paper and video explainer from a few months ago.

https://www.microsoft.com/en-us/research/blog/claimify-extra...

What about proven facts that get disproven? Is there room to rethink your priors?

I think for that kind of thing, Prolog would be sufficient. Lean is more powerful, but it requires you to supply proofs - Prolog can just automatically run inferences.

(Although I wouldn't be surprised if somebody had already recreated something like Prolog in Lean with a tactic that does more or less what the Prolog interpreter does)

Look at Arguman, now defunct, but you can probably find some good videos/screenshots.

Basically crowd-sourced statements, rebuttals, agreements, etc, in a nice interface.

We need that nowadays.

I think a more practical method would be to trace the provenance of a claim, in a way that lets you evaluate how likely it is for the person making it to actually know the facts.

A simple scenario would be reading a news article about american politics. You see an unusual claim made, so you start tracing it and find that the journalist got it from person X who got it from person Y who got it from donald trump. Trump is famous for lying constantly, so unless there's a second source making the claim, you could disregard it with a high probability.

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

As a programmer who has studied philosophy: This is the approach I take more or less in my head when reading articles, however the problem is the ambiguity of natural language.

E.g. lets say the statement is about a presidents promise to end a conflict within 24 hours after coming into office. One could get to a conclusion pretty quickly when the conflict hasn't been ended after 24 hours when they entered the office.

But what does "end the conflict" mean exactly? If the conflict ended how long does it need to remain ended to achieve the label "ended"? What if said president has a history that recontextualizes the meaning of that seemingly simple claim because he is known to define the word "ended" a little different than the rest of us, do you now judge by his or by our definition? What if the conflict is ended but there is a small nest of conflict remaining, after which size do we consider the conflict going on?

I know some of that has official definitions, but not everything has. In the end a lot of that will require interpretation and which definition to chose. But yeah I support your idea, just spelling it out and having a machine-readable chain of thought might help already.

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.

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.

The article mentions it, in fact: https://adam.math.hhu.de/#/g/leanprover-community/nng4

> 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.

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.

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.

[1] https://steamcommunity.com/app/2262930

> 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.

Take a look at zeroth-order logic.

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.

Some good mentions elsewhere in the thread, another to check out is The Incredible Proof Machine https://incredible.pm/

Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.

> so are we basically compiling a dictionary of proofs all stemming from a handful of self-evident truths

I would say, "from a handful of axioms".

It's certainly true that when Euclid started this whole enterprise, it was thought thax axioms should be self-evident. But then, many centuries later, people discovered that there are other interesting geometries that don't satisfy the same axioms.

And when you get to reasoning about infinities, it's very unclear that anything about them can be considered self-evident (a few mathematicians even refuse to work with infinities, although it's definitely a very niche subcommunity).

Some of today's common axioms are indeed self-evident (such as "you should be able to substitute equal subterms"), but things like the axiom of choice have (at least historically) been much more controversial. I would probably say that such axioms can be considered "plausible" and that they generally allow us to be able to prove what we want to prove. But you'll definitely find mathematicians championing different axioms.

> 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.

That would be the ZFC axioms. It was originally the ZF axioms (named so after the mathematicians Zermelo and Fraenkel who worked in the early 20th century), and then later the Axiom of Choice (C) was added. It's generally considered to be the "standard" set of axioms for maths, although very few mathematicians actually work directly from these axioms. But in theory, you can take almost every mathematical proof (unless it's explicitly set in some other foundation) and recast it entirely in applications of the ZFC axioms.

You probably are vaguely referencing the Principa Mathematica.

How are you asking questions like this and yet you're a roboticist and a principal software engineer in the autonomous mobile robotics industry.

From your questions I marked you as a high schooler.

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!

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.

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?

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?

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.

This is why I prefer Agda, where everything comes down to pattern matching.

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.

You may like Agda. I prefer Lean even though you are right about this.

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-...

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.

> 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/ Which gives a way to do the clicking-through outside the editor. And maybe gives some insight into how Lean people see things.

Rocq used to have a "mathematical proof language". It's hard to find examples, but this shows the flavor (https://stackoverflow.com/a/40739190):

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.

Isabelle's Isar proof language is similar, and AFAIK the standard way of proving in Isabelle (example from https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-...):

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed

I don't know if there is anything like this for Lean, but maybe this provides some keywords for a web search. Or inspiration for a post in some Lean forum.

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

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.

Thanks!

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 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/) and 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.

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.

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.

This is an active area of research and experimentation!

Much of Lean community are on Zulip (which is kind of like a forum?) and you can see many relevant threads here: https://leanprover.zulipchat.com/#narrow/channel/219941-Mach...

For now I'm just learning math with it!

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).

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.

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

Apparently this is possible with macros? I dunno: https://github.com/leanprover/lean3/issues/1355

Work is already underway in that direction:

https://github.com/deepseek-ai/DeepSeek-Prover-V2

but also

https://deepmind.google/discover/blog/alphaevolve-a-gemini-p...

Terence Tao is doing a lot of work in this direction.

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-th... though the issue has since been fixed.

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.

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

[2] https://www.cs.ru.nl/%7Efreek/100/

[3] https://mizar.uwb.edu.pl/100/

There are a few.

The lean one is at https://github.com/leanprover-community/mathlib4

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.

>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

Fermat's Last Theorem is easily solved with css. Just do:

    margin-left: 200px;