What VR is¶

VR is mathematics built from operations alone. It posits no axioms of its own. Its Lean 4 library, VR, has stood on the empty axiom list since 2026-09-12/13, and a guard enforces this at build time (the exact scope of the guard is below). VR covers more than arithmetic: it also builds the integers, rationals and reals, a set universe, a continuum on Brouwer's path, point-free topology, and a two-register account of formal statements.

The author is Vitaly Reznik. The work was formalized and written with Claude (Anthropic). The author directs the work and is responsible for it. The VR cycle is finished and parked. This page describes what is published and what is in the code. Code: inventor1975/VRCycle. VR has a single author, no peer review and no citations; read it as a machine-checked research programme, not as established mathematics.

Nothing is — all is doing¶

VR does not start from things. It starts from acts. ∅ is the nullary operation, the act that takes no operands. It is not an empty thing. 0 is that act, 1 = t(∅) is one application of succession to it, and n is n applications. The source says it at the type itself, in VR/Arithmetic.lean: "No ontology is ascribed."

The claim has a limit, and the project's own compass (VR-LOGIC.md) states it. VR has no ontology of substance. The set layer still makes commitments, such as a global membership relation and potential infinity. These are tracked, not denied.

What "without axioms" means¶

No axioms of its own. VR has two primitives, base (∅) and succ (t). Membership ∈ is defined by recursion, not assumed. Succession (A3) is proved (A3_mem_self, A3_subset_succ). Induction (A4) is the recursor of the inductive type (A4_induction), not a postulate.
Over a framework. Lean's type theory (inductive types and recursion) is the framework and the checker. "Without axioms" means that no declaration uses any of Lean's three declared axioms (propext, Quot.sound, Classical.choice) and none uses sorry. It does not mean "without a framework".
No Mathlib. The VR library imports nothing but Lean itself. The few borrowed basics (Set, Nat.find, ∃!) are rebuilt in VR/Prelude/.
Guarded. VR/Guard.lean runs #assert_axiom_free_library VR. Since 2026-10-30 it checks every constant of the library — private and auto-generated ones included — and exempts only the listed tool code (tactic programs in VR.Meta.CSRNorm and VR.Meta.DependsOn, and the notation macro ⌜·⌝), naming each exempt constant in its output. Measured on 2026-10-30 at commit 1f1f629: "2623 constants checked, all on [] … 73 exempt as tool code". Before that day the guard skipped declarations that mention Lean's own library and all private ones; a census then found one automatically generated lemma with propext (IntExpr.mk.injEq, now removed) and one private test instance with Quot.sound (now on []), both fixed the same day.
Check it yourself. Clone the repository and run lake build VR. The first build also downloads Mathlib, because the second library needs it; VR does not import it. To check one theorem, open a file that imports VR and run #print axioms VR.Theorem_11_VR_PA. Lean answers that it does not depend on any axioms.
The classical register is separate. A second library, VRClassical, holds everything stated about Mathlib objects or built with quotients. Its axioms are the standard ones, declared per object. VRClassical depends on VR, and VR does not depend on VRClassical.

One limit of the check itself: the guard is a Lean metaprogram. It is trusted the same way #print axioms is trusted. It is not a kernel-checked proof.

What VR builds¶

Everything in this table is in the guarded VR library, so all of it is on the empty axiom list.

Area	What the code establishes	Where
Arithmetic	The natural numbers from `∅` and `t`. VR is equivalent to Peano arithmetic through an explicit `Nat ≃ VRObj` that preserves 0, successor, +, × and ^ (`Theorem_11_VR_PA`).	`VR/Arithmetic.lean`
ℤ, ℚ, ℝ	Integers as pairs of VR numbers, rationals as pairs of those, and reals as Cauchy sequences with an explicit modulus. Identity is a witnessed relation (`intEq`, `qEq`, `rEq`), not a quotient. The code proves ring laws, order and apartness, and builds the reciprocal of a positive real (`rinvPos`). These reals have no trichotomy.	`VR/Numbers/{IntegersOp, IntegersOrd, RationalsOp, RealsOp}.lean`
Sets	A set is a pointed graph, read as a revealing functionality (`OpSet`). Identity is a witnessed bisimulation (`OpSet.Equiv`). Well-foundedness is a property of a set (`IsGrounded`), not an axiom, so ZFC-style and ZFA-style sets live on one carrier. Anti-foundation is a theorem (`OpSet.afa`). The universe is not enumerable (`OpSet.universe_not_enumerable`).	`VR/SetsOp/`
Continuum (Brouwer)	Infinite binary branches are not enumerable (`branches_not_enumerable`). The countable performed nodes cannot cover them (`no_node_surjection`). Both are combined in `operational_cantor`. Continuity holds for finite-information functionals (`continuity_of_nbhd`). Uniform continuity is proved only conditionally, with Brouwer's continuity and fan principles as explicit hypotheses (`uniform_continuity`); they are never adopted. Dependent choice holds when it is given by a rule (`operational_dependent_choice`).	`VR/Continuum/`
Topology	Point-free formal topology with coverage, compactness, continuous maps and products, and the binary Tychonoff theorem (`tychonoff_binary`).	`VR/Topology/`
Forms	Operational and formal registers. The formal register is conservative over the operational one, proved in three storeys: propositional, first-order, and comprehension. The way from operational to formal is proved (`translate_implies_realisable`). For the way back, no general mechanism is known.	`VR/Forms/`
Apparatus	The two operationality modes and two transit modes (Mode A, Mode B) as Lean classes and definitions.	`VR/Apparatus/`
ZTL layer	VR's sets and branches read through Zero-Trust Logic. See VR and ZTL.	`VR/ZTL/`

Some things are not in the guarded library. They live in VRClassical, where the standard axioms are allowed and declared per object:

the isomorphisms with Mathlib's ℤ, ℚ, ℝ and ℂ;
the complex layer, which is only the Gaussian rationals ℚ(i): the witnessed layer GaussE is itself on [], but it lives in VRClassical (it imports a classical module) and is not covered by the guard; its quotient bridge GaussQ uses Quot.sound (VRClassical/Continuum/GaussianRational.lean). The published VR-Numbers paper describes ℂ over ℝ; the code has only ℚ(i);
the quotient bridges Qop, GaussQ and Real;
the ZFC reading over Mathlib's ZFSet;
the refutation of Brouwer's continuity in the classical register (not_continuity);
the Hahn–Banach audit;
Brouwer's fixed-point theorem over Mathlib's ℝ.

What is open¶

These items come from VR-LOGIC.md §3 and §4, the project's own list.

Are formal terms operational? A description of something with no operational counterpart, such as ℘(ℕ) as a completed totality or full choice, may itself be an operational act, or it may be something else. This is not settled.
Bishop or Brouwer? The continuum follows Brouwer: the branches are not enumerable. The reals are Bishop-style Cauchy reals. The exact relation between the two is open.
The operational reals are incomplete. There is no completeness or least-upper-bound theorem yet, and no trichotomy.
From formal back to operational. No general mechanism exists. Proof mining covers some cases. It fails where a classical proof selects without a rule.
CH and full choice. These are discussed in the essays, not in the code. The code covers the diagonal, dependent choice by a rule, and continuity.
Reach. The method is shown in arithmetic, sets, analysis, algebra and topology. Whether it extends to all of mathematics is a conjecture.
Maturity. It is small next to Mathlib. The operational reading is argued in prose, outside the Lean statements; "VR is equivalent to Peano arithmetic" is proved inside Lean, so it shows relative strength, not an independent foundation.

Published works¶

All works are on Zenodo, by Vitaly Reznik. For each work the table gives two DOIs. The concept DOI always resolves to the newest version. The version DOI points to the exact newest version as of 2026-10-30. Versions and concept DOIs were read from the Zenodo API, and every DOI below was checked on 2026-10-30: doi.org answers with a 302 redirect to Zenodo.

Work	Newest version	Concept DOI (all versions)	Version DOI
VR. A Formal System: An Axiom-Free Reconstruction of Arithmetic from Operations Alone	1.1.1 (2026-06-14)	10.5281/zenodo.20212091	10.5281/zenodo.20688164
VR-Numbers: Operational Superstructures of Integers, Rationals, Reals, and Complex Numbers over the Natural Numbers of VR	1.1.1 (2026-06-14)	10.5281/zenodo.20272025	10.5281/zenodo.20688749
VR-Sets: An Operational Set Theory Unifying ZFC and ZFA (Brouwer Edition)	1.1.0 (2026-06-11)	10.5281/zenodo.20303535	10.5281/zenodo.20643407
VR-Sets-ZFA: Operational Reference Semantics for Non-Well-Founded Sets	1.0.1 (2026-06-01)	10.5281/zenodo.20369345	10.5281/zenodo.20485610
VR-Forms: An Operational Two-Register Apparatus over VR-Sets	1.0.3 (2026-10-25)	10.5281/zenodo.20313734	10.5281/zenodo.23647163
VR-Audit: A Programme of Operational Audits of Classical Theorems	1.0.1 (2026-06-01)	10.5281/zenodo.20364110	10.5281/zenodo.20485556
VR-Apparatus: A Machine-Verified Apparatus for the Operational Methodology of the VR Cycle	1.0.0 (2026-05-25)	10.5281/zenodo.20381416	10.5281/zenodo.20381417
VR-Algebra: Operational Tracking Discipline Applied to Algebraic Structures	1.0.0 (2026-05-26)	10.5281/zenodo.20398299	10.5281/zenodo.20398300
VR Part II: Raising VR onto Zero-Trust Logic	1.0.0 (2026-07-12)	10.5281/zenodo.21326037	10.5281/zenodo.21326038
Choice as an Act: Russell's Socks, Cardinals as Becomings, and the Productive Continuum, Machine-Checked on the Empty Axiom List	1.0 (2026-07-17)	10.5281/zenodo.21419289	10.5281/zenodo.21419290

Three further works are released as code only. They have git tags in the repository and no Zenodo record:

VR-Topology (v1.13-vr-topology-v1.0.0);
VR-Transit (v1.15-vr-transit-v1.0.0);
Brouwer's fixed-point theorem via Sperner's lemma (v1.16-vr-brouwer-v1.0.0).

The early works also have Lean-companion records on Zenodo from May 2026. These are snapshots of older code. The repository is current.

Papers against code. All papers except VR-Forms 1.0.3 were published before the library-wide move to the empty axiom list (2026-09-12/13). Choice as an Act (July) claims the empty list for its own theorems; the guard over the whole library came later. Where a paper gives an axiom profile or a file path that differs from the repository, the repository and its guard are current.