ΘρϵηΠατπ

Principles

Why Human-Written Mathematics Still Matters

Modern proof systems such as Lean are remarkable because they can check every formal step. That is valuable work, and Openmath is not a rejection of it. Openmath exists because there is still a good reason for people to write mathematical thoughts, definitions, and proofs in a form meant first for human readers.

A machine-checked proof is optimized for certainty inside a formal system. A human-written page can do something different: it can explain why a definition is natural, which example to keep in mind, how one result should be used later, and what idea makes a proof work. Those choices are not opposed to rigor. They are part of how people understand mathematics.

Iterative Correctness

In a proof assistant, the formal statement and proof must satisfy the system before the work is accepted. That discipline is powerful, but it also means the writer has to work in a precise formal language from the start. A proof either checks or it does not, and it can be hard to feel finished with the work until the system accepts it.

Openmath has a different advantage: pages can begin as readable mathematical explanations and improve over time. Someone who has the right idea for a proof, but does not yet know how to complete every detail, can still write down the route they see. That contribution can be useful immediately, and another person can later clarify the hypotheses, fill in the missing argument, add links to earlier definitions, or turn the explanation into a fuller proof.

This does not mean that correctness is optional. It means that correctness can be approached iteratively. Openmath gives contributors a way to make meaningful progress before the proof is perfect, while still leaving a path toward increasingly precise arguments.

Future Tools

We expect mathematical tools to keep improving. It seems likely that future systems will be able to read a human-oriented knowledge base and convert parts of it into formal structures. Once that becomes possible, those systems may help find logical gaps, inconsistencies, missing hypotheses, circular reasoning, or places where two pages do not quite fit together.

Instead of requiring every contributor to work inside a proof assistant right now, Openmath focuses on writing useful mathematics now. The hope is that human-readable definitions, proofs, and explanations can eventually be checked, translated, or assisted by stronger tools without losing the value of the human writing that came first.

Openmath should not encourage carelessness. Assumptions, proof gaps, and unclear arguments should be made visible and improved. The point is only that human mathematical writing has value even when it is not machine checked. It gives us a place to write down the ideas, motivations, and proof structures that people can learn from and refine.

Working principles