Machine-Native Reasoning · Reviewed Mathematical Core
From an observation to accountable revision
A sensor displays one bit under an unknown convention. Follow that small example through what a record determines, what a representation preserves, what correction requires, and which decisions and revisions the retained evidence supports.
Read the reviewed core · Find a statement or written proof
A first reading path
- Begin with accessible evidence and a reusable state
- See what memory must keep for later correction
- Put one inquiry under an explicit resource budget
- Track which results remain applicable after a revision
Know the scope of the edition
The retained reader develops 27 selected results with complete written proofs across nine chapters. Its 12 counterexamples keep the boundaries visible. The current MachineTheory companion contains a root import and 78 mathematical modules; the statement map identifies the modules and declarations attached to each selected result.
Read what the review label means · Inspect the recorded formal scope · Browse all current Lean files
The accepted project pins Lean 4.34.0-rc2. The browser checker uses Lean 4.33.0 as a separate experiment, with some required imports unavailable. Reproduce the recorded environment with the retained compiler and dependency instructions. Read the portable reproduction instructions
Continue through the whole argument
Read the chapters in order to connect representation, correction, decision, inquiry, discovery, revision, and shared obligations. The final source chapters retain the author’s source relationships and limits.
Open the complete core contents · Read the result and source map
Original publication and wider continuation
The original PDF retains the printed publication. The wider research continuation is a separate edition with its own evidence and review boundaries; the selected-core correspondence does not certify the wider manuscript.
Open the reviewed-core publication and companion records · Open the wider continuation
This reading conversion reports retained evidence. It adds no proof review, Lean execution, or empirical validation.