(en.wikipedia.org) Mizar system - Wikipedia

ROAM_REFS: https://en.wikipedia.org/wiki/Mizar_system

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.

In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.

Local Graph

org-roam 84a83fd6-8983-49fa-8694-49a0ace2f4b0 (en.wikipedia.org) Mizar system - Wik... //en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Formal_language 84a83fd6-8983-49fa-8694-49a0ace2f4b0->//en.wikipedia.org/wiki/Formal_language //en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant 84a83fd6-8983-49fa-8694-49a0ace2f4b0->//en.wikipedia.org/wiki/Proof_assistant //en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking 84a83fd6-8983-49fa-8694-49a0ace2f4b0->//en.wikipedia.org/wiki/Automated_proof_checking //en.wikipedia.org/wiki/Mathematical_formalization https://en.wikipedia.org/wiki/Mathematical_formalization 84a83fd6-8983-49fa-8694-49a0ace2f4b0->//en.wikipedia.org/wiki/Mathematical_formalization //en.wikipedia.org/wiki/Andrzej_Trybulec https://en.wikipedia.org/wiki/Andrzej_Trybulec 84a83fd6-8983-49fa-8694-49a0ace2f4b0->//en.wikipedia.org/wiki/Andrzej_Trybulec 2a07e4ea-610b-4c9a-bb84-d961fb2450e5 Code and Coffee Book Club 2a07e4ea-610b-4c9a-bb84-d961fb2450e5->84a83fd6-8983-49fa-8694-49a0ace2f4b0