Language models support search, translation and explanation but never certify correctness. They can propose definitions, identify similar theorems, decompose a goal, generate examples and explain a verifier's failure in accessible language. Symbolic systems perform algebraic computation; specialised solvers handle constrained domains; proof assistants check formal derivations against explicit foundations. A provenance layer records which system produced each step and what guarantees it carries. Adversarial agents actively seek counterexamples and hidden assumptions. The useful intelligence lies in routing a question to the right mode of reasoning and preserving boundaries between them, so that fluency accelerates discovery without acquiring the visual authority of proof.
Proof
“What if mathematics were a collaborative medium, not a solitary language?”
The beginning
Proof is an exploratory environment for moving between intuition, diagrams, computation and formal reasoning. Mathematical work rarely begins in the syntax in which it is finally published: it begins with examples, visual hunches, analogies, failed constructions and half-formed invariants. Current tools divide that process. Proof assistants demand precision but offer little support for discovering what to formalise; conversational models offer fluency but can make invalid reasoning feel complete. Proof would preserve the productive uncertainty of exploration while creating a visible path towards verification. It treats mathematics as a collaborative medium in which a learner, researcher, machine and community can share objects, transformations and questions without confusing suggestion with truth.
The distance between informal understanding and formal proof excludes many people from advanced mathematics and slows experts working across unfamiliar fields. A diagram may contain the essential insight but no machine-readable structure. A symbolic result may be correct but offer no explanation of why it matters. A language model may propose a convincing proof with a subtle gap that only appears several steps later. Existing notebooks separate prose, code and formal verification into adjacent cells rather than one coherent reasoning object. The deeper problem is epistemic: mathematical software often hides the status of a statement. Conjecture, numerical evidence, computer-verified lemma, imported theorem and intuitive analogy can appear with the same visual authority.
What it could become
The product would be a visual notebook built around conjectures rather than documents. Users create mathematical objects, draw relationships, generate examples, request counterexamples and expose proof obligations as a navigable dependency graph. Every statement carries a visible status and provenance. A diagram can be translated into candidate formal structures; computation can test finite cases; a language model can suggest lemmas or explanations; and a proof assistant can certify the parts expressed within its foundations. Multiple representations remain synchronised, allowing a user to move from geometry to algebra or from an intuitive animation to exact definitions. Collaboration focuses on unresolved obligations, alternative proof strategies and explanations that connect formal steps back to the original insight.
For whom
- University students learning proof
- Researchers exploring unfamiliar domains
- Engineers working with formal methods
- Teachers designing mathematical explanations
Core capabilities
- Diagram-to-structure interpretation
- Symbolic computation and theorem search
- Counterexample generation
- Formal proof assistant integration
The project becomes meaningful only when a new technical possibility is translated into a clear human advantage, an experience people can understand, and a system capable of earning trust over time.
Intelligence and mathematics
Mathematics is both the content and the interface. Objects are represented through types, invariants, transformations and dependency graphs; category-theoretic ideas can connect equivalent constructions across representations; graph search explores possible lemma paths; and automated theorem proving ranks tactics without hiding the final derivation. Counterexample generation uses constraint solving and finite-model search. Uncertainty about an informal claim remains explicit until its quantifiers and assumptions are defined. The system could measure proof complexity, identify structurally central lemmas and show where several arguments share the same underlying pattern. Its success is not the number of automatically solved exercises but the degree to which users can see why a statement is true, false or still genuinely open.
How it might live
Proof could begin with university courses where the gap between intuition and formal reasoning is especially visible. A freemium learner workspace would support examples, diagrams and guided obligations; institutions would pay for course libraries, collaboration, assessment integration and locally governed models. A research edition could add large formal libraries, private workspaces and domain-specific tooling for software, hardware and scientific verification. The long-term asset would be a graph of verified explanations linking human intuition to formal objects, not a corpus of answer text. Partnerships with proof-assistant communities and universities would be essential: the company should strengthen open mathematical infrastructure rather than enclosing foundational knowledge behind a proprietary chat interface.
For me, a venture is more than an interesting technology. It needs a narrow first user, a repeated problem, a distribution path, a credible advantage and a reason to improve as more people use it. I would test those conditions before deciding whether this idea should become a company, a product, an open technology or an ongoing research programme.
Rules for making it real
- 01
A beautiful explanation is not a proof.
- 02
Counterexamples are first-class outcomes.
- 03
Every formal step should remain connected to intuition.
- 04
Uncertainty must be visible in the interface.
From question to company
- 01Frame
Build conjecture, example and counterexample notebooks.
- 02Prototype
Integrate a first proof assistant.
- 03Prove
Pilot with undergraduate proof courses.
- 04Build
Open researcher workspaces and shared verified libraries.
What could go wrong
Serious imagination includes the possibility that an idea should change radically—or should not exist. These are the tensions the project would need to resolve:
- Users trusting fluent but unverified reasoning.
- Optimising for solved exercises rather than understanding.
- Narrow formal systems excluding valuable mathematical practice.