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!
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.)