4Leibniz / Calculemus
Kernel-oriented formal knowledge graph with transparent proof search, typed epistemic status, and dependency-aware arguments.
Universal-calculus workspace
Author a claim, search only the declared premises, and inspect the exact proof steps or remaining obligations.
Live deduction REPL
Run compile, prove, or explain against the current claim. Results remain JSON-auditable.
Semantic patch preview
Patches transform meaning-bearing claim structures, not raw source text.
Epistemic status lattice
Click a node to inspect its rank. Edges show permitted weakening toward lower certainty.
Argument dependency graph
Click a theorem node to inspect its module and epistemic status.
Phase 4 collaborative calculus
AI suggestions are advisory and unverified. Consensus records dissent and never replaces Lean kernel checking.
Phase 3 failure analysis
For an unproved claim, search a bounded integer model or compare two semantic revisions.