An auditable guide to the abc conjecture and IUT
This repository turns the original research plan into a reading path. Its subject is Mochizuki's published, contested claim to prove abc using inter-universal Teichmüller theory (IUT). It is not a new proof, an endorsement of the disputed inference, or a claim that publication or a Lean formalization has settled the dispute.
Start here: Project map and evidence rules → The abc target → Prerequisite route → IUT source route → Claim dependencies → The contested step → Lean's boundary → XI-001's gated status → XI-002's native-\(q\) trace. A reader already comfortable with heights, valuations, and elliptic curves can skip the prerequisite route, but should not skip the source or dispute status labels.
What is available
| File | What the reader gets |
|---|---|
| Project map | The questions, dependency directions, and evidence labels |
| The abc target | Definitions, worked examples, an elementary equivalence proof, and the conditional Szpiro bridge |
| Prerequisite route | A selective study path with exercises and stopping points |
| Polynomial abc lab | An optional, complete proof of an instructive analogy, not of abc over integers |
| IUT source route | A source-located first pass through the published claim and its limits |
| Claim dependencies | Paper-side nodes and arrows to verify, not an established proof graph |
| The contested step | Side-by-side primary-source accounts of the IUT III disagreement, without a verdict |
| Lean boundary | A pinned, conditional formalization audit, including the unproved input |
| Lean dependency ledger | Pinned theorem edges, assumptions, build evidence, and explicit unaudited dependencies |
| Lean vocabulary | Typed counterparts for a few terms, not authoritative IUT definitions |
| Working dictionary | Standard definitions, comparison cautions, and IUT-specific reading questions |
| Research queue | The ten stages from the plan reorganized into verifiable tasks and review gates |
| Critical-mechanism audit | A typed object/transport ledger, conditional map-to-bound reduction, diagram, and deliberately limited toy models |
| Object-identity ledger | The six distinct SS real-line nodes, IUT III's hull, a source-paired arrow crosswalk, and explicit unresolved maps |
| Adversarial trial | Independent source readings, a dependent formalizer's test, and the exact remaining proof obligations |
| XI-001 gated experiment | Independent readings, separate source and mathematical gates, rejected shortcuts, and the first unresolved native-\(q\) comparison |
| XI-002 native-\(q\) trace | A frozen-source, arrow-by-arrow attempt to relate the fixed input value to the bounded output, with a normalization mini-audit and an exact stop point |
| Source register | Checked references, pending audits, and a citation policy |
| Original plan | The motivating proposal; its citations and claims require independent checking |
The IUT claim graph, the competing interpretations of its critical step, and the scope of the Lean work are separate source-audit tracks. Their current guides are first passes, not proof-level verification of every edge. In particular, do not fill an unresolved arrow from the original plan's diagram.
How to use this repository
Read a mathematical statement together with its source locator, logical
status, and remaining obligation. A published proposition, a derivation
we can reproduce, and a Lean theorem conditional on a proposition are three
different kinds of evidence. In particular, a checked implication
Corollary 3.12 variant -> abc does not check Corollary 3.12 itself.
Each substantive guide now places a Graduate-level walkthrough (intuition only) near its opening, after the page's scope or audit result. Read it for a worked mental model and prerequisite links, then continue into the source-paired argument and its precise stop point. The walkthroughs, videos, and informal references do not change an evidence label or independently verify a disputed IUT inference; the prerequisite route collects optional starting resources.
The goal is a sequence of explanations that a mathematician can challenge at a specific arrow, not a simplified story that hides the arrow. Text here is original commentary and links to the source material, not a copy of the papers. Snapshot of this reading path: 2026-10-06.
Run the reading site (hosting, not mathematical evidence)
The source repository contains both the research guide and the site configuration. This section explains how to host the guide; running a server provides no evidence for a mathematical claim. The site uses Material for MkDocs, MathJax for equations, and Mermaid for claim diagrams. For a local preview with Python 3.11 or later:
python -m pip install -r requirements-docs.txt
python -m mkdocs serve
Open http://127.0.0.1:8000/. Edits to the README, plan, or guide are
reflected in the preview. MathJax is loaded from unpkg.com in the browser;
Material also loads Mermaid from that CDN, so the browser must be able to
reach it to render equations and diagrams. To build a static copy, run
python -m mkdocs build --strict. Only the README, original plan, guide
Markdown, and site JavaScript are staged for publication. _sources is
excluded from the Docker build context, and infrastructure files are not
served by the final image.
To serve the production image locally (with a running Docker daemon):
docker build -t abc-guide .
docker run --rm -p 8080:8080 abc-guide
The workflow in .github/workflows/publish-image.yml publishes
ghcr.io/talaatharb/abc:latest and a commit-SHA tag on pushes to master,
including PR merges. On first publication, set the GHCR package's
visibility to public in its package settings; repository access does not
automatically make the image public. The workflow publishes an image but
does not deploy it.
The Kubernetes manifests in k8s require an nginx ingress controller,
cert-manager with a letsencrypt-prod ClusterIssuer, and DNS for
abc.talaatharb.net pointing to the ingress. After the public image is
available, run kubectl apply -f k8s to create the Deployment, Service,
and TLS Ingress. After later image publishes, run
kubectl rollout restart deployment/abc-docs to pull the new latest tag;
publishing alone does not restart existing pods.