4 ms·

I've played around with Coq before, and it's really hard to work with mathematics in it. If you start with a system of axioms in first order logic(like groups),

I've played around with Coq before, and it's really hard to work with mathematics in it. If you start with a system of axioms in first order logic(like groups), it's pretty easy to prove single things. But once you start wanting to quantify over all subgroups, you're in trouble. I remember seeing a presentation where someone challenged the viewer to write a simple proof of the infinitude of the primes. I recommend you try it. I studied math in college, have an interest in formal proofs, and have written Coq code, so surely I could bang out a simple proof like that. I think I got stuck when I wanted to claim, "Given a natural number n, x <= n implies x = 0 or x = 1 or ... or x = n". It's possible that I have more experience now and could complete that proof if I tried again, but this is really the kind of thing they teach on the first day of an introduction to proofs course. I can't see mathematicians using theorem provers until they're easier to work with. So I sympathize with and am rooting for Voevodsky here: There's no reason why theorem provers have to be a pain to use - we just need better foundations, better tools, and more experience using them.

darkmighty 11y ago
Perhaps that could be a new 'job' in itself? "Proof programmer": persons specialized in formalizing proof statements. So if you're an experienced PP maybe the statement above becomes easy. Or you use a proof in a 'library' of sorts that let's you proof that. If 1) Proofs are well defined enough in the first place that you don't need great insight to understand them; 2) The time of some mathematicians is very invaluable; 3) Formalizing/verifying statements is sufficiently useful for mathematicians; then they might be useful?
- ende 11y ago
  I can see the headline now... "Show HN: Pudding - A language for programming proofs". I could see a lot of uses for this kind of programming. In a language like Matlab or R, we just assume that the implementations correctly match the theoretical methods they implement, but anyone who has deleved into the internals of some published R library knows that's not always the case. With the expanded use of pure functional languages for more closely mapping method to implementation, proof programming could offer a useful form of unit testing to the development of libraries.
raverbashing 11y ago
Well, maybe it has to do with the ways of "proving" infinitude of primes, of that it is a "high level description" and more importantly, writing it so that other, future theorems can avail to it. Think of all you need to prove that: the natural numbers, the definition of addition, subtraction, multiplication, division (and remainder), definition of cardinality/infinity (might not be necessary, if you just need proof that N doesn't divide any numbers between 2 and N-1) and a lot of formal logic
yaantc 11y ago
The typical way to prove that there is an infinity of primes is to do a reductio ad absurdum: you assume there is a finit number of primes, call the biggest P and build another bigger one that is prime. This is a contradiction, so you can conclude that there is no highest prime and hence there is an infinity of them. The thing here is that this uses the law of the excluded middle: a proposition is either true or false, there is no other possibility. That's the basis of a proof using reduction ad absurdum. But that's not part of Coq (or any P.A. based on constructive logic) by default. If one is not aware of this indeed doing this proof will be impossible in Coq. This said Coq can work with the law of excluded middle (so support classical logic), but you have to explicitly assert it and use it. This being said, I haven't tried this proof in Coq ;) Just seeing this point as something to take into account, and that may be a problem for some people new to Coq and not aware of it.
- Chinjut 11y ago
  Proving NOT P by showing a contradiction follows from P is perfectly fine in intuitionistic logic (the sort used in Coq), and not dependent upon the law of the excluded middle in that sense. What's not available to you is proving P by showing that a contradiction follows from NOT P (rather, you end up with NOT NOT P, which is not assumed to entail P simpliciter).
  - digama 11y ago
    I believe that in the context of the infinitude of primes, this is the difference between "NOT (finitely many primes)" and "infinitely many primes", where "infinitely many" means that the primes are in bijection with the natural numbers (and of course finitely many means in bijection with some natural number). A proof by contradiction will only give the weaker first statement in intuitionistic logic. One explanation for why many people say that Euclid's proof is not a proof by contradiction is because you can actually get the second statement with only a little more care (i.e. n!+1 has a prime divisor, which is thus greater than n).
vegedor 11y ago
> this is really the kind of thing they teach on the first day of an introduction to proofs course It's not definitely taught using constructive logic, nor would the proof be rigorous I guess. I've just had a look at Isabelle/HOL and would be just as tempted to assume it a feasible task. But then, the amount of code in the example theorem for Eratosthenes' Sieve is quite huge compared to a verbal introduction and some jotted down notes on the black board.
digama 11y ago
For what it's worth, here's a proof that the primes are unbounded (and hence infinite) in the proof language Metamath: http://us.metamath.org/mpegif/prmunb.html http://us.metamath.org/mpegif/prmunb.html . I would classify myself as a "proof programmer" who works with Metamath for much the same reasons as people use Coq (I just happen to prefer Metamath's set theory foundations to type theory). I find the article's claim "Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs" as outright false for this reason. Mizar is another set theory-based proof system. If I wanted to prove x <= n -> x = 0 or x = 1 or ... or x = n, I would use http://us.metamath.org/mpegif/leloe.html http://us.metamath.org/mpegif/leloe.html to turn x <= n <-> x < n or x = n, and http://us.metamath.org/mpegif/zltlem1.html http://us.metamath.org/mpegif/zltlem1.html to prove x <= n-1 from x < n. Repeat until you get down to zero to get all n cases.
- sukilot 11y ago
  What is "all n cases" when you are quantifying over all "n"?. There are an infinitude of cases. You need induction.

darkmighty 11y ago

Perhaps that could be a new 'job' in itself? "Proof programmer": persons specialized in formalizing proof statements. So if you're an experienced PP maybe the statement above becomes easy. Or you use a proof in a 'library' of sorts that let's you proof that. If 1) Proofs are well defined enough in the first place that you don't need great insight to understand them; 2) The time of some mathematicians is very invaluable; 3) Formalizing/verifying statements is sufficiently useful for mathematicians; then they might be useful?

ende 11y ago
I can see the headline now... "Show HN: Pudding - A language for programming proofs". I could see a lot of uses for this kind of programming. In a language like Matlab or R, we just assume that the implementations correctly match the theoretical methods they implement, but anyone who has deleved into the internals of some published R library knows that's not always the case. With the expanded use of pure functional languages for more closely mapping method to implementation, proof programming could offer a useful form of unit testing to the development of libraries.

raverbashing 11y ago

Well, maybe it has to do with the ways of "proving" infinitude of primes, of that it is a "high level description" and more importantly, writing it so that other, future theorems can avail to it. Think of all you need to prove that: the natural numbers, the definition of addition, subtraction, multiplication, division (and remainder), definition of cardinality/infinity (might not be necessary, if you just need proof that N doesn't divide any numbers between 2 and N-1) and a lot of formal logic

yaantc 11y ago

The typical way to prove that there is an infinity of primes is to do a reductio ad absurdum: you assume there is a finit number of primes, call the biggest P and build another bigger one that is prime. This is a contradiction, so you can conclude that there is no highest prime and hence there is an infinity of them. The thing here is that this uses the law of the excluded middle: a proposition is either true or false, there is no other possibility. That's the basis of a proof using reduction ad absurdum. But that's not part of Coq (or any P.A. based on constructive logic) by default. If one is not aware of this indeed doing this proof will be impossible in Coq. This said Coq can work with the law of excluded middle (so support classical logic), but you have to explicitly assert it and use it. This being said, I haven't tried this proof in Coq ;) Just seeing this point as something to take into account, and that may be a problem for some people new to Coq and not aware of it.

Chinjut 11y ago
Proving NOT P by showing a contradiction follows from P is perfectly fine in intuitionistic logic (the sort used in Coq), and not dependent upon the law of the excluded middle in that sense. What's not available to you is proving P by showing that a contradiction follows from NOT P (rather, you end up with NOT NOT P, which is not assumed to entail P simpliciter).
- digama 11y ago
  I believe that in the context of the infinitude of primes, this is the difference between "NOT (finitely many primes)" and "infinitely many primes", where "infinitely many" means that the primes are in bijection with the natural numbers (and of course finitely many means in bijection with some natural number). A proof by contradiction will only give the weaker first statement in intuitionistic logic. One explanation for why many people say that Euclid's proof is not a proof by contradiction is because you can actually get the second statement with only a little more care (i.e. n!+1 has a prime divisor, which is thus greater than n).

vegedor 11y ago

> this is really the kind of thing they teach on the first day of an introduction to proofs course It's not definitely taught using constructive logic, nor would the proof be rigorous I guess. I've just had a look at Isabelle/HOL and would be just as tempted to assume it a feasible task. But then, the amount of code in the example theorem for Eratosthenes' Sieve is quite huge compared to a verbal introduction and some jotted down notes on the black board.

digama 11y ago

For what it's worth, here's a proof that the primes are unbounded (and hence infinite) in the proof language Metamath: http://us.metamath.org/mpegif/prmunb.html http://us.metamath.org/mpegif/prmunb.html . I would classify myself as a "proof programmer" who works with Metamath for much the same reasons as people use Coq (I just happen to prefer Metamath's set theory foundations to type theory). I find the article's claim "Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs" as outright false for this reason. Mizar is another set theory-based proof system. If I wanted to prove x <= n -> x = 0 or x = 1 or ... or x = n, I would use http://us.metamath.org/mpegif/leloe.html http://us.metamath.org/mpegif/leloe.html to turn x <= n <-> x < n or x = n, and http://us.metamath.org/mpegif/zltlem1.html http://us.metamath.org/mpegif/zltlem1.html to prove x <= n-1 from x < n. Repeat until you get down to zero to get all n cases.

sukilot 11y ago
What is "all n cases" when you are quantifying over all "n"?. There are an infinitude of cases. You need induction.