4 ms·

I agree with this wholeheartedly. The down side is that it's going to take forever to get everyone on board. Mathematicians are very hostile to outside influenc

I agree with this wholeheartedly. The down side is that it's going to take forever to get everyone on board. Mathematicians are very hostile to outside influences. Constructive mathematics should be more of a thing too.

danharaj 7y ago
How do you figure?
- adamnemecek 7y ago
  Old school mathematicians don't understand the value of theorem provers and aren't all that excited about learning it.
  - danharaj 7y ago
    Understandable. I've been fucking with them for years as a professional programmer and I think they suck eggs.
    - adamnemecek 7y ago
      I agree but so does the math syntax.
  - ncmncm 7y ago
    The problem might be that once you try to get your theorem into a proof system, you're not doing maths anymore: now you're programming. Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard. Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already. We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever. Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof? Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system. Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering. Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?
jewelry 7y ago
I don't think Mathematicians themselves didn't like this idea. In fact Hilbert tried it (https://en.wikipedia.org/wiki/Hilbert%27s_program https://en.wikipedia.org/wiki/Hilbert%27s_program) one hundred years ago and it failed and proved to be not possible. Well maybe the Hilbert program is too aggressive, and this Lean thing is much moderate. But at the end of the day, the boundary of what program solver could do is bounded already hence no one is paying too much attention.
- adamnemecek 7y ago
  Things get nicer when you accent constructive mathematics. I (I'm not the only one) think that Hilbert was wrong.
- joycian 7y ago
  Aren't humans bounded in the same way? Why not build a system that's faster than us?
Animats 7y ago
Yes. Been there, done that, a long time ago, and had the same political problems. Many years ago, around 1980, I headed a project to build one of the first program proof of correctness systems. (It's on Github now, about two-thirds working with modern compilers.)[1] We succeeded, but it was just too hard to use. And, back then, really slow. As in 15 minutes to hours. We had two theorem provers. One was what's now called an SMT solver - it could prove theorems with addition, subtraction, multiplication by constants, equalities, inequalities, and the Boolean operators. It could also accept rewrite rules, which it accepted as true. Because allowing users to input rewrite rules made it easy to create false proofs, we required that the rewrite rules be proven using the Boyer-Moore theorem prover, which is a pure constructive system.[2] Then the theorems could be transferred to the SMT solver and used there. One of the things we set out to prove were the "axioms" for arrays. There are four, credited to McCarthy in his classic 1962 paper. But we wanted to prove them from a theory of constructive arrays. In Boyer-Moore theory, we defined arrays as sorted lists of (subscript, value) tuples. And then we set out to prove the classic four axioms for arrays with machine proofs. Which we did.[3], starting at line 3372. That file is the Boyer-Moore theorem prover grinding its way up from a very low base of number theory to the theorems we needed for our program proving system. (On a modern computer, in seconds. Took 3 hours on a VAX in 1980. We just didn't have enough engine for this stuff back then.) In that notation, "(selecta A I)" means A[I], and "(storea A I V)" is array A with A[I] replaced with V. After some struggles, we got the the prover to find a way to prove that. But it's ugly. There's lots of case analysis, which mathematicians hate. We didn't get to redefine "equal", so we couldn't have abstract sets. We had to have ordered lists of tuples, which meant all the fussyness of updating an ordered list representation and proving that was sound. But it all worked. So I submitted this to JACM, back when that mattered. It was rejected. The comments were along the lines of "I don't like having something that ugly at the foundations of computer science". The reviewers all agreed it was valid, but they just didn't like doing it that way, in an automatic but inelegant way. Looks like the author of the original article here is still having that problem. Good times back then. But we were way ahead of our time. [1] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temporaryrulebaseprooflog.txt https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

danharaj 7y ago

How do you figure?

adamnemecek 7y ago
Old school mathematicians don't understand the value of theorem provers and aren't all that excited about learning it.
- danharaj 7y ago
  Understandable. I've been fucking with them for years as a professional programmer and I think they suck eggs.
  - adamnemecek 7y ago
    I agree but so does the math syntax.
- ncmncm 7y ago
  The problem might be that once you try to get your theorem into a proof system, you're not doing maths anymore: now you're programming. Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard. Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already. We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever. Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof? Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system. Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering. Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?

jewelry 7y ago

I don't think Mathematicians themselves didn't like this idea. In fact Hilbert tried it (https://en.wikipedia.org/wiki/Hilbert%27s_program https://en.wikipedia.org/wiki/Hilbert%27s_program) one hundred years ago and it failed and proved to be not possible. Well maybe the Hilbert program is too aggressive, and this Lean thing is much moderate. But at the end of the day, the boundary of what program solver could do is bounded already hence no one is paying too much attention.

adamnemecek 7y ago
Things get nicer when you accent constructive mathematics. I (I'm not the only one) think that Hilbert was wrong.
joycian 7y ago
Aren't humans bounded in the same way? Why not build a system that's faster than us?

Animats 7y ago

Yes. Been there, done that, a long time ago, and had the same political problems. Many years ago, around 1980, I headed a project to build one of the first program proof of correctness systems. (It's on Github now, about two-thirds working with modern compilers.)[1] We succeeded, but it was just too hard to use. And, back then, really slow. As in 15 minutes to hours. We had two theorem provers. One was what's now called an SMT solver - it could prove theorems with addition, subtraction, multiplication by constants, equalities, inequalities, and the Boolean operators. It could also accept rewrite rules, which it accepted as true. Because allowing users to input rewrite rules made it easy to create false proofs, we required that the rewrite rules be proven using the Boyer-Moore theorem prover, which is a pure constructive system.[2] Then the theorems could be transferred to the SMT solver and used there. One of the things we set out to prove were the "axioms" for arrays. There are four, credited to McCarthy in his classic 1962 paper. But we wanted to prove them from a theory of constructive arrays. In Boyer-Moore theory, we defined arrays as sorted lists of (subscript, value) tuples. And then we set out to prove the classic four axioms for arrays with machine proofs. Which we did.[3], starting at line 3372. That file is the Boyer-Moore theorem prover grinding its way up from a very low base of number theory to the theorems we needed for our program proving system. (On a modern computer, in seconds. Took 3 hours on a VAX in 1980. We just didn't have enough engine for this stuff back then.) In that notation, "(selecta A I)" means A[I], and "(storea A I V)" is array A with A[I] replaced with V. After some struggles, we got the the prover to find a way to prove that. But it's ugly. There's lots of case analysis, which mathematicians hate. We didn't get to redefine "equal", so we couldn't have abstract sets. We had to have ordered lists of tuples, which meant all the fussyness of updating an ordered list representation and proving that was sound. But it all worked. So I submitted this to JACM, back when that mattered. It was rejected. The comments were along the lines of "I don't like having something that ugly at the foundations of computer science". The reviewers all agreed it was valid, but they just didn't like doing it that way, in an automatic but inelegant way. Looks like the author of the original article here is still having that problem. Good times back then. But we were way ahead of our time. [1] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temporaryrulebaseprooflog.txt https://github.com/John-Nagle/pasv/blob/master/src/work/temp...