You can support this project by donating at:

Or see the list of project sponsors.

bourbakimath

Documentation	😀
Docstrings	🥺
Tests	🥺
Examples	😀
RepositoryActivity	🥺
CI	🥺

This is the system for verifying formal mathematical proofs. As I didn't use math since the high school and lack time to dive into the lengthy documentation :(

Here is the code snippet from the example:

;; Declare the wff type
(symkind "WFF")

;; The implication symbol
(prim wff "->" (wff ![x y]))

;; the axioms
(ax "ax1" (wff ![A B])
  (ass [-> A -> B A]))
(ax "ax2" (wff ![A B C])
  (ass [-> -> A -> B C -> -> A B -> A C]))

;; the rule of inference (modus ponens)
(ax "ax-mp" (wff ![A B])
  (hypo [A] [-> A B])
  (ass [B]))

;; theorem: identity law for '->'
;; compare with id1 in set.mm
(th "id" (wff "A")
  (ass [-> A A])
  (proof
    [ax1 A [-> A A]]
    [ax2 A [-> A A] A]
    [ax-mp [-> A -> -> A A A]
           [-> -> A -> A A -> A A]]
    [ax1 A A]
    [ax-mp [-> A -> A A] [-> A A]]))

If you eval it in the REPL, then you can verify it and output some information:

BOURBAKI-USER> (print-theorem !id)
Theorem id:
Variables: A
Distinct variable conditions: 
Hypotheses: 
Assertion: [-> A A]
Proof:
ax1 [A][-> A A]
ax2 [A][-> A A][A]
ax-mp [-> A -> -> A A A][-> -> A -> A A -> A A]
ax1 [A][A]
ax-mp [-> A -> A A][-> A A]

BOURBAKI-USER> (show-proof !id)
Proof for id:
ax1 => [-> A -> -> A A A]
ax2 => [-> -> A -> -> A A A -> -> A -> A A -> A A]
ax-mp => [-> -> A -> A A -> A A]
ax1 => [-> A -> A A]
ax-mp => [-> A A]

BOURBAKI-USER> (verify !id)
Theorem: "ax1"
Theorem: "ax2"
Theorem: "ax-mp"
Theorem: "id"
T

Bourbaki has a very good documentation. If you are interested in math libraries and don't know how to spend this weekend - enjoy it:

https://www.quicklisp.org/beta/UNOFFICIAL/docs/bourbaki/doc/bourbaki-3.7.pdf