The Curry Howard isomorphism says that given a programming language with a expressive type system, a correspondence can be defined between propositions with types on the one hand, and proofs and programs on the other. In other words, we can express any mathematical claim as a type whose truth is proven by its instantiation.
This means that a compiler can be used as a proof-checker. If the proof represented by the instantiation was invalid, then compilation should fail.
Organization
* There is some old experimental stuff I did in Scala a long time ago before I was fully prepared to build this thing for real.
* include/logic/intuitionistic.hpp : intuitionistic logic is a version of logic where propositions are about the existence of a proof rather than about truth.
* include/math/number/natural/peano.hpp : the peano axioms of the natural numbers.
Further plans:
* finiteness
* prime numbers
* algebraic structures such as groups, rings, and fields.
* cyclic, symmetric, and alternating groups
* integers and rationals
* cauchy sequences
* real numbers and calculus.
* linear algebra
* complex numbers
* affine spaces
* exterior algebra
* differentials
* spinors
* combine linear algebra and groups to get representation theory
* combine linear algebra with algebra to get Galois theory
* combine linear algebra with calculus to get differential geometry
* finally can get to real math when comlplex analysis, differential geometry, and number theory all work together.