I am new to the world of computer assistant proof programs in general, and Coq in particular. As a result, I have sought to prove some elementary results about integers as a way to … At the moment, I ...
After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof. We can express proofs as a computer program Proof is correct ...
While looking for a way to visualize the logical structure of mathematical theories a graph-like depiction came to my mind, where propositions are represented by vertices. An edge goes from ...
I am looking for a math editor that is able to present equations and relations between them. I am not searching for a traditional Latex / MathML editor (I know about various online services that allow ...
I recently read about the 4 color theorem and that it was proved using help from computers. Does anybody know of some other 'good' computer-assisted proofs apart from the 4 color theorem?