math-o-matic

docs · main page

English · 한국어

math-o-matic is a computerized deductive system that enables you to make an axiomatic system and prove its theorems. Its aim is to make it easy to write and read rigorous mathematical proofs. You can see the current axiomatic system by pressing one of the buttons at the bottom of the main page.

Code example

"[$1+1=2]이다."
theorem one_plus_one_is_two() {
    one_in_omega()
    > omega_add_one(omega_one) as eq(omega_add(omega_one, omega_one), omega_two)
}

The above code produces…

A proof of 1 + 1 = 2

…a proof of the equation 1 + 1 = 2. The proof is verified by the math-o-matic program, and the name of the theorem is colored green if the proof is valid. The proof explorer also shows the individual steps of the proof in a human-readable format. The names in green refer to theorems that are already proved, and the symbols in blue are predefined notions.

Keep reading

• Find more math-o-matic code in /math directory.
• Refer to the documentation to learn how to write proofs.
• Click on the colored parts of the proof above in the main page to jump to definitions.
• math-o-matic language support for Visual Studio Code and Sublime Text 3 can be found in /tools.

Contributing

A lot of theorems need proofs. Please open a pull request after you prove new theorems.

Refer to CONTRIBUTING.md for more information.