3

Sorry for the noob question: does it exist an automatic proof checker?

I mean, some kind of programming language that validates the steps of a proof.

I don't speak of automatic proof finder, just a way to computationally validate a proof, using axioms and previously validated proofs.

What I search is a way of making proofs that kinds of reasembles programming a computer.

Edit: Thanks for the answers. I'll try to clarify what I am searching. I admit I don't see it clearly myself. I don't want it to easily verify homework. That for sure. I have much more experience as a programmer than making proofs. Whoever I see similarities between the two.

I don't search exactly for a formal proof checker. That is way too hard to use. Maybe something more similar to unit testing that validates some results.

When I program, I can then compile and run the program, and both steps give me tips as to where I made a mistake, or if there is no mistake and everything works. And with object-oriented language I can give the program an 'archotecture' (decide what object can do what needed action)

A math book seems similar to an object-oriented program, where the autor decides its chapters and objects with axioms, definitions and from that some propositions and later theorems are proved.

What I search is a 'way of coding' that validates, maybe not all but at least part of what I'm writing is correct. And allows me to maybe change the architecture I'm giving what I'm writing.

I have read about COQ software, but it is too dificult to learn. I want the language to be able to abstract ideas, so that reading it feels like reading a book. And only if I want I can go check the technical details.

Maybe even with some known existing language like python could something be made ? I imagine an 'VectorSpace' object, a Field object, a Group object. Proofs would be routines expanding the api, for example the proof of the unicity of identity element of a group would be added to the Group object.

I can't find the way to code what I want (not even clearly see what I want) but I can't find where the dificult lies. I feel that it should be possible.

Thanks for your time reading all this!

dami
  • 486
  • Not really. People have played around with this, but to my knowledge it is not computationally feasible currently. Here is a website where you can explore how terrible this topic is. In particular, the proof that $2+2=4$ involves $2,913$ "subtheorems" (whatever that means) http://us.metamath.org/mpegif/mmset.html – pancini Nov 19 '19 at 23:39
  • 3
    @ElliotG I have not used it myself, but a lot has been accomplished in Mizar: "As of July 2012, the MML included 1150 articles written by 241 authors. In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have so benefited from formal codification. Some examples are the Hahn–Banach theorem, Kőnig's lemma, Brouwer fixed point theorem, Gödel's completeness theorem and Jordan curve theorem." – Jair Taylor Nov 19 '19 at 23:58
  • I stand corrected then; I didn't realize it was that powerful. My point was more that you cannot yet verify a proof using wolfram alpha or something. Also I don't mean to belittle their work; it sounds super cool, but definitely not the field for me. – pancini Nov 20 '19 at 00:03
  • May I humbly suggest my DC Proof 2.0 freeware. More info and free download at http://www.dcproof.com – Dan Christensen Nov 20 '19 at 17:59
  • I am afraid that tools like Coq is your only way. There is no “informal proof checker”. It is an illusion that mathematics written in natural languages is easier to understand. Proofs in textbooks are incomplete and ambiguous. While reading them, not only you need to understand them, but also you need to fill in the gaps and resolve ambiguities on your own. If you can do this, reading a formal proof is easy-peasy. A proof tool may be hard to use, but this is not because it works with formal statements and proofs. It is a UI problem. – beroal Feb 27 '20 at 19:10

2 Answers2

4

It sounds like what you're looking for is a proof assistant, a list of which can be found on Wikipedia as a starting place.

As ElliotG noted in the comments, creating fully formalized proofs like this for nontrivial theorems is still generally considered quite difficult and a field of active research. (In particular, if you want this to, e.g., check homework proofs, it's probably going to create much more work for you than it saves.)

Gregory J. Puleo
  • 6,443
1

Yes, such tools exist and have been used to verify some famous theorems. See Gonthier's proofs of the Four-Color Theorem and of Feit–Thompson theorem. However, such tools are very difficult to use. See this question for more details.

J.-E. Pin
  • 40,163
  • The question you linked is more closely to what I wanted to ask than what I really asked. Thanks. I edited my question adding more detail – dami Nov 20 '19 at 20:04