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. 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 |
| 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.
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-05.
Reading site
The site renders the Markdown with 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.