Plural by construction
Multiple proofs, formulations, translations, relations, and axiom profiles are first-class objects.
Lean 4 knowledge infrastructure
Verified mathematics needs plural infrastructure.
MathVLT turns isolated Lean declarations into a source-preserving research graph where proofs, formulations, dependency routes, axiom profiles, explanations, translations, and communities can coexist.
Lean verifies mathematics.
VLT structures its plurality.
MathVLT connects it globally.
Project philosophy
Formal truth should not collapse mathematical plurality.
MathVLT starts from a simple premise: verification is necessary, but not enough. Mathematical research also needs durable ways to compare alternatives, preserve provenance, explain meaning, and let communities curate locally without deleting valid work.
Proposition-proof separation
A proof points to a separately registered proposition, so one statement can retain many valid routes.
Local canonicalization
Venues and users can choose preferred views for their context without erasing alternatives globally.
Provenance before popularity
Source lineage, environment, authorship, and verification status stay attached to every object.
The four stages
One data model, four independent products.
The project is not a monolithic app. Each layer has its own value, and each layer can stand on the layer below without forcing private work into a global service.
Lean projects
VLT
VLT-View
MathVLT
mathvlt.com
Stage 01
VLT
Lean architecture for variation, linking, and translation.
A package, protocol, and project convention for registering propositions, proofs, relations, semantic artifacts, dependency signatures, axiom footprints, provenance, and exports.
Stage 02
VLT-View
A local-first interface for ordinary Lean and VLT projects.
A standalone viewer that renders projects as navigable mathematical systems, with proposition pages, proof comparison, semantic views, dependency graphs, and provenance.
Stage 03
MathVLT
The normalized global corpus and knowledge graph.
A public registry that ingests supported Lean sources, preserves environments and source history, normalizes objects conservatively, and connects related material across projects.
Stage 04
mathvlt.com
The hosted research network built on the corpus.
A platform for search, profiles, venues, discussion, curation, collaboration, voting, moderation, private spaces, and model-attributed AI sessions anchored to formal objects.
Research network
A living map, not another theorem browser.
MathVLT is connective architecture between Lean, mathlib, repositories, papers, research groups, and AI systems. It keeps formal validity central while making explanation, attribution, comparison, and collaboration persistent.
What the network preserves
- Alternative proofs and dependency antichains.
- Per-proof axiom footprints and statement-level summaries.
- Semantic artifacts: explanations, translations, examples, and notation views.
- Source occurrences with repository, file, commit, declaration, and environment.
What it refuses to do
It does not replace Lean, mathlib, papers, or research communities. It does not force one canonical definition, proof, notation, or explanation. It gives researchers a substrate where local standards can coexist with global plurality.