 # Lisp Project of the Day

## bourbaki

### 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

Brought to you by 40Ants under 