Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why formalize mathematics – more than catching errors

rkirov.github.io

Post reply on HN
Print view View original

21–30 of 80 posts

Re: Why formalize mathematics – more than catching errors

#21

Post by kronicum2025 »

vonnik wrote: post #10
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…

Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?

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.

Re: Why formalize mathematics – more than catching errors

#22

Post by nomilk »

Related: Terrence Tao discussing Lean (programming language for formalising mathematical proofs) on Lex podcast (starts 1h20m): https://www.youtube.com/watch?v=HUkBz-cdB-k&t=1h20m10s

I know nothing of mathematics but found it fascinating, especially the idea that if outside information changes that affects your proof, you can have the Lean compiler figure out which lines of your proof need updating (instead of having to go over every line, which can take days or more).

Re: Why formalize mathematics – more than catching errors

#24

Post by wslh »

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?

https://en.wikipedia.org/wiki/List_of_incomplete_proofs?wpro...

Re: Why formalize mathematics – more than catching errors

#25

Post by [deleted] »

lo_zamoyski wrote: post #11
bwfan123 wrote: post #6

Earlier quoted context omitted.

Bessis [1] argues that formalism - or loosely math writing - is foundational to clarifying intuition/meaning in a way that natural language cannot. Imagine it as a scalpel carving out precise shapes from the blur of images we carry thereby allowing us to "see" things we otherwise cannot. I am curious to try out lean to understand how definitions in lean are able to operationally capture meaning in an unambiguous mann…

For mathematics and certain fields, that is true. But the formalism matters, and as some have argued, the Fregean style that came to dominate in the 20th century is ill-suited for some fields, like linguistics. One argument is that linguists using this style inevitably recast natural language in the image of the formalism. (The traditional logical tradition is better suited, as its point of departure is the grammar o…

[deleted]

Re: Why formalize mathematics – more than catching errors

#27

Post by eig »

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?

Re: Why formalize mathematics – more than catching errors

#28

Post by kachnuv_ocasek »

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?

Lean has much better UX to be frank. Rocq is fine, but if I were to start formalising today, I'd pick Lean.

Re: Why formalize mathematics – more than catching errors

#29

Post by mlpoknbji »

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 that (most) mathematicians were not that interested in formal proof until quite recently (as opposed to computer scientists), and most of the interest in lean has been self-reinforcing, namely there is a (relatively speaking) huge library of formally verified mathematics. So now basically anyone who cares about formal verification as a tool for mathematics is working in lean. There are of course numerous techincal differences which you can read about if you google coq vs lean.

Re: Why formalize mathematics – more than catching errors

#30

Post by Ericson2314 »

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?

Rocq is ancient and has some longstanding UX problems. It is pleasant to try making a new code base.

This is kinda like asking, why write Clang when we already had GCC? Or, why making Python if we already have Perl?

It's good to have some competition for these things, Rocq I believe felt the heat and has been also doing some good things in recent years.

Post reply on HN