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

Building the Mathematical Library of the Future

quantamagazine.org

Post reply on HN
Print view View original

31–40 of 47 posts

Re: Building the Mathematical Library of the Future

#31

Post by mturmon »

roywiggins wrote: post #16
mturmon wrote: post #13

Earlier quoted context omitted.

One of the usual examples given in reaction to this question is the puzzle of Euclid's 5th postulate, the parallel-lines postulate. People tried for centuries to prove that it could be deduced from the other axioms. Turned out, it was independent of the others. A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, whic…

At best an proof-checker can invalidate a purported proof, it absolutely is not going to prove that no proofs are valid (it would have to affirmatively prove that the result is actually independent of the axioms you picked, which is a lot harder)

Many incorrect proofs of this postulate were given over the years. (For instance, in some cases these erroneous proofs have steps that implicitly use the postulate itself.)

The proof checker could detect such errors in a purportedly clean proof.

Re: Building the Mathematical Library of the Future

#32

Post by dwheeler »

yaseer wrote: post #4

There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178 When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem. With computer aided proofs, I do wonder if the multitu…

There are indeed several different proof systems. "Formalizing 100 Theorems" tracks the progress of the "top" ones compared to a set of well-known proofs:

http://www.cs.ru.nl/%7Efreek/100/

The top ones (sorted from most to least complete) are HOL Light, Isabelle, Metamath, Coq, Mizar, and Lean. Lean actually has the fewest proofs of those systems, though of course there are advantages to Lean as well.

I think some duplication is inevitable because there are fundamental disagreements on "what is important".

One problem with most of them as a "store of proof knowledge" is that most of these proof systems don't (normally) store the proof in terms of axioms, definitions, and previously-proven theorems. Instead, they store a program (as a sequence of tactic statements) that, if run, is intended to help the prover rediscover the proof... assuming that tactics never change (even though they do). As a result, older proofs in some of these systems can no longer be verified as being correct. This is one thing that attracts me to Metamath; Metamath stores literally every step, with all mathematical knowledge (including all axioms and definitions) in the database, so proofs stay proven. It also makes verification super-fast, e.g., 28K theorems can be verified in less than 1 second.

Others believe other traits are important, so they end up with different systems.

As far as translations between systems, I'm very interested in what happens with Metamath Zero. That work might, in the end, enable mutual translations between various systems. We'll see!

Re: Building the Mathematical Library of the Future

#33

Post by Ericson2314 »

leafmeal wrote: post #27

As I understand, Lean is a dependently typed programming language. How does it compare to a language like Idris? How come mathematicians are encoding math in Lean instead of Idris for example? Someone please correct me, I don't know much about this at all, but I was under the impression that Lean is in a more "imperative" style, while Idris is a functional language. I would have guessed that a functional language wou…

I think the "imperative" part is the tactics—metaprogram invocations, the underlying language is still functional.

Idris is geared more towards programming than theorem proving, with the difference basically being that with the latter one cares about more than the types ("I didn't formalize my spec completely") so the specific inhabitant matters. That makes tactics a bit dangerous.

Now there is also a school of thought the finds this reliance on metaprogramming (imperative of other) ugly and a site indication the languages and libraries are not good enough yet. I'm sympathetic, but currently the pro-tactic crowd seems to have the edge.

Lastly, "Lean" is kind of the epitome of "success at all costs" in more ways than tactics: implementation in C++ rather than a nice functional language for dogfooding, willing to sacrifice some intuitionist sacred cows not strictly needed for classical compatibility, etc.

Re: Building the Mathematical Library of the Future

#34

Post by leanuser83 »

dwheeler wrote: post #32
yaseer wrote: post #4

There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178 When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem. With computer aided proofs, I do wonder if the multitu…

There are indeed several different proof systems. "Formalizing 100 Theorems" tracks the progress of the "top" ones compared to a set of well-known proofs: http://www.cs.ru.nl/%7Efreek/100/ The top ones (sorted from most to least complete) are HOL Light, Isabelle, Metamath, Coq, Mizar, and Lean. Lean actually has the fewest proofs of those systems, though of course there are advantages to Lean as well. I think some du…

(Disclaimer: I'm addicted to Lean. My view is biased.)

Note that Lean is not so high on that list, but also note that serious theorem proving in Lean is less than 5 years old, whereas the other systems are (several) decades old. There are at least two entries on the list that have only been formalized in Lean, and not in any other system. We are catching up pretty quickly.

It's clear that this list has an important status. But in my opinion, building a library of undergrad maths, which is what what TFA is mainly about, is a lot more important. We are tracking our progress over at https://leanprover-community.github.io/undergrad.html

I am not aware of such an organized effort in other systems. Without such a fleshed-out undergrad library, we'll never get to systematic formalization of (post)grad mathematics.

Re: Building the Mathematical Library of the Future

#35

Post by delusional »

yaseer wrote: post #4

There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: https://cordis.europa.eu/project/id/742178 When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem. With computer aided proofs, I do wonder if the multitu…

The exact same thing is said about other programming languages.

Re: Building the Mathematical Library of the Future

#36

Post by digama0 »

Ericson2314 wrote: post #33
leafmeal wrote: post #27

As I understand, Lean is a dependently typed programming language. How does it compare to a language like Idris? How come mathematicians are encoding math in Lean instead of Idris for example? Someone please correct me, I don't know much about this at all, but I was under the impression that Lean is in a more "imperative" style, while Idris is a functional language. I would have guessed that a functional language wou…

I think the "imperative" part is the tactics—metaprogram invocations, the underlying language is still functional. Idris is geared more towards programming than theorem proving, with the difference basically being that with the latter one cares about more than the types ("I didn't formalize my spec completely") so the specific inhabitant matters. That makes tactics a bit dangerous. Now there is also a school of thoug…

> implementation in C++ rather than a nice functional language for dogfooding

To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure functional) language. The siren song is strong :)

Re: Building the Mathematical Library of the Future

#37

Post by Strilanc »

ezequiel-garzon wrote: post #7
edgyquant wrote: post #2

I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making…

What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.

You could ask questions that would normally take hours or days or years to know the answer to, and have the answer immediately. Sure you still need to work on understanding why, but you'd only work on understanding why for something correct. How could that not lead to a stronger intuition?

Re: Building the Mathematical Library of the Future

#38

Post by bolus »

ezequiel-garzon wrote: post #7
edgyquant wrote: post #2

I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making…

What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.

First of all, mathematics is not about T/F. Think of the axiom of choice, the law of excluded middle, the axiom of inaccessible cardinals, etc.

For the second, understanding why and actually proving something can be related but they're not equivalent. Of course, the intuitive ideas can lead to the right formal technicalities but it is not always the case.

There are two aspects of mathematical proofs-communication of ideas and formal verification. Confusing these distinction can be dangerous and this is why mathematicians led to the area of type theory and formal proofs.

Voedovsky, you can google him to find who he was, lost his faith in "human proof checking" after some error on his peer-reviewed and published result was accidentally discovered after years of nobody doubting its validity.

He dreamed of the world where people do and enjoy mathematics freely leaving the boring parts to computers like mathematicians in nowadays don't worry about how their writing will be published and communicated. What we do is write a proof and leave actual typesetting to the computer. It's called (La)TeX.

What you're saying is like claiming this program is correct because its logic is correct without ever knowing whether the code itself would get compiled or not. More extremely, there's no value for having more and more pseudocodes that we don't know they'll ever terminate or not.

Re: Building the Mathematical Library of the Future

#39

Post by Smaug123 »

Koshkin wrote: post #17
ezequiel-garzon wrote: post #7

Earlier quoted context omitted.

What do you gain from automated proofs? Take the infinitude of primes. Plenty of textbooks different proofs of this fact to deepen your insight. Having an oracle-like entity tell me whether something is true or false is unlikely to have the same result, and I’m afraid “following the automated proof” won’t help much in this regard.

> automated proofs You've got a point, but in this case you are barking at the wrong tree. Aren't they talking about automated proof- checking ?

Yes, though waves hands machine learning can in principle be used to create a proof-generator from a proof-checker.

Re: Building the Mathematical Library of the Future

#40

Post by emrehan »

ahelwer wrote: post #21

Lean is the basis for my favorite puzzle game of the past five years: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... It's like enemies & bosses are mathematical theorems you have to prove. Each time you slay one, you get it as a weapon you can use against further, more difficult bosses! The grand finale (Inequality World) is very memorable; such a feeling of accomplishment after I cracked it all. The…

How many hours does it take to complete?
Post reply on HN