I'm working through Terence Tao's Real Analysis textbooks which start from Peano's axioms and build up from there and I was wondering can I use Coq to formalise and verify my proofs but without having to learn the existing libraries? I would like to start from scratch: enter the same axioms and then to refer only to them and to the previously proven statements in my proofs. The book uses set-theoretic framework.

  • 3
    $\begingroup$ that would be quite obscene in my opinion $\endgroup$ – Jorge Fernández Hidalgo Oct 25 '17 at 15:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.