Why formalize mathematics – more than catching errors • Hacker News Board

Re: Why formalize mathematics – more than catching errors

#61

Post by thaumasiotes » Sat, Oct 25, 2025, 2:20 AM UTC

oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

> I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods.

> Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what to use them for and how.

How is any of that different from what we had in math before Lean?

Re: Why formalize mathematics – more than catching errors

#62

Post by thaumasiotes » Sat, Oct 25, 2025, 2:25 AM UTC

konne88 wrote: post #38

I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.

> Maybe better tactics will help. I'm not sure.

I don't see why they would.

If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.

Re: Why formalize mathematics – more than catching errors

#63

Post by vonnik » Sat, Oct 25, 2025, 3:13 AM UTC

vonnik wrote: post #53

kronicum2025 wrote: post #21

Earlier quoted context omitted.

I'm leaning a lot into AI + lean. It's a fantastic tool to find new proofs. The extremly rigid nature of lean means you can really check programs for correctness. So that part of AI is solved. The only thing that remains is generating proofs, and that is where there's nothing in AI space right now. As soon as we do get something, our mathematical knowledge is going to explode.

What kind of math do you do, and what would “generating proofs” look like do you think?

i don't know why this was down-voted... i'm genuinely interested in the answers. feel free to dm me.

Re: Why formalize mathematics – more than catching errors

#64

Post by lanstin » Sat, Oct 25, 2025, 3:58 AM UTC

skybrian wrote: post #41

js8 wrote: post #34

Earlier quoted context omitted.

I just had a similar discussion with a coworker, he was advocating that LLMs are practically useful, but I argued they are kinda bad because nobody knows how they really work. I think it's somewhat return to pre-enlightenment situation where the expert authority was to be taken for their word, there was no way to externally verify their intuitive thought process, and I believe success of science and engineering is ba…

The project to formalize everything has been tried before and abandoned. Some issues: https://metarationality.com/sort-of-truth Formalism isn't the right tool for a lot of semi-factual fields like journalism or law. Even in business, numbers are of course used in accounting, but much of it depends on arbitrary definitions and estimates. (Consider depreciation.)

Lawyers (here on HN) have said that contracts that specify everything are too expensive to come up with. Better to cover the most common cases and have enough ambiguity so that weird eventuality end up litigated.

Re: Why formalize mathematics – more than catching errors

#65

Post by lanstin » Sat, Oct 25, 2025, 4:02 AM UTC

thaumasiotes wrote: post #61

oersted wrote: post #3

I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what…

> I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods. > Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on…

It is more software ish. You don't just have a citation to earlier results, you can import the library. And you don't have to trust collaborators as much, the proof engine validates. And you can use github to coordinate large projects with incremental but public progress.

Re: Why formalize mathematics – more than catching errors

#66

Post by aureianimus » Sat, Oct 25, 2025, 5:06 AM UTC

lordnacho wrote: post #36

Noob question here. Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation? If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check? I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tes…

In a lot of cases you can get far by locally proofreading the definitions.

Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.

Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.

Re: Why formalize mathematics – more than catching errors

#67

Post by aureianimus » Sat, Oct 25, 2025, 5:26 AM UTC

eig wrote: post #27

I’m not a mathematician, so could someone explain the difference in usage between Lean and Coq? On a surface level my understanding is that both are computer augmented ways to formalize mathematics. Why use one over the other? Why was Lean developed when Coq already existed?

I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.

Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it. I consider this matter to be an open question.

If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.

The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around. My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.

Re: Why formalize mathematics – more than catching errors

#68

Post by aureianimus » Sat, Oct 25, 2025, 5:30 AM UTC

gtsnexp wrote: post #26

Ask HN: What’s the single best resource for learning Lean (beyond the official docs)?

All the good resources are listed here: https://lean-lang.org/learn/

I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.

If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant

Re: Why formalize mathematics – more than catching errors

#69

Post by robinzfc » Sat, Oct 25, 2025, 6:11 AM UTC

fouronnes3 wrote: post #23

Is there, somewhere, a list of theorems that were considered proved and true for a while, but after attempts at formalization the proof was invalidated and the theorem is now unknown or disproved?

There was a question [1] on mathoverflow about this with a couple of interesting answers and comments.

[1] https://mathoverflow.net/questions/291158/proofs-shown-to-be...

Re: Why formalize mathematics – more than catching errors

#70

Post by anonymousDan » Sat, Oct 25, 2025, 9:34 AM UTC

jojomodding wrote: post #58

anonymousDan wrote: post #55

I don't get the point about trivial proofs. Can't you just tell Lean to assume something is true and then get on with the rest of the interesting part?

You can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.

Yeah I guess it's more a question of methodology for me. You have several parts of a proof, and your intuition guides you that certain parts are more likely to be risky than others. Better to get those straight first since you've a higher chance of failure (potentially rendering much of the work you have already done pointless). Then you can come back to flesh out the hopefully more straightforward parts. This is as opposed to taking a purely bottom-up approach. At least that's how I often tackle a complex coding problem - I am no mathematician!