Strong Artin: source and evidence

General Strong Artin remains open. Historical checkpoints are separate formal projects.

Completion: Reading edition complete · Lean: Inherited / related evidence · Confidence: Historical formal evidence

Before you start

Suggested background: Read the problem statement, recorded scope and open questions first. The program's definitions determine its subject prerequisites.

Recorded results and limits: Finished evidence reader with retained scoped formal results. The publication records zero fresh Lean invocations and global automorphic attachment remains open.

Remaining work: Restore the exact runtime and replay the current source, then keep the global carrier-existence input as a separate research obligation.

The background advice is an editorial starting point. The work itself states its prerequisites and hypotheses.

Reading routes · Glossary · Claim links · Download this work

Read

• Edition README
• Read PDF
• Visual guide (PDF)

Back to work navigation

Written proofs

Read the written arguments in the PDF. The manuscript source remains available below.

Find the statement number or section in the reading files, then read its assumptions and argument. A claim map may cover only part of the written result.

• Manuscript text (TeX)

Find this work among other written proofs

Back to work navigation

Lean

Start with the edition guide and the build instructions below. Check the correspondence records to see which written claims the Lean declarations cover. Source links lead to .lean files. PDF guides explain the formalization.

• Formal source guide and replay prerequisites
• v0.38 checkpoint mathematical modules
• All retained formal checkpoints and ancestry

Find this work among other Lean projects

Back to work navigation

Code

These links include code, examples, checks, or build tools. Read the edition guide for setup instructions and what each command does. All software is beta and work in progress.

• Script: build.py

Find this work among other code projects

Back to work navigation

Evidence

• Completion, Lean coverage, confidence, and cited evidence
• Source-file receipt (identity and availability)
• All files in this source edition

The evidence records describe the reviews and runs completed for this edition.

Back to work navigation

Continue browsing

• Previous: Streaming Polyphase Factor Decomposition / SKAT
• Next: Physics: curvature states
• Back to Research programs
• All collections