v0.3.0: Lean and Mathlib v4.35.0, 110 modules

LeanFrontier on Lean and Mathlib v4.35.0: 110 accepted modules, up from 102 in v0.2.0, all admitted mechanically by the receiver.

Using it

[[require]]
name = "LeanFrontier"
git = "https://github.com/carlok/LeanFrontier.git"
rev = "v0.3.0"

lake update
lake exe cache get   # Mathlib's prebuilt files; without it, lake build compiles Mathlib
lake build

import LeanFrontier brings in everything, and each subject module can also be imported alone. This release was validated with a fresh downstream Lake project pinned to this commit. It fetched the Mathlib cache, built, and #checked entrypoints from the first accepted submission to the newest.

New since v0.2.0

• Furstenberg topology and the profinite completion. The arithmetic-progression topology on ℤ is identified with the topology of all finite-index quotients, and Mathlib's canonical map into the profinite completion is a dense embedding inducing it (isDenseEmbedding_furstenbergProfiniteMap).
• Stern–Brocot paths and continued fractions. Path runs give the full Euclidean quotient sequence, and Mathlib's GenContFract.of of a path's rational is the finite continued fraction of those runs (genContFract_pair).
• Geometry. Curvature-centre circles with tangency, bridging the Descartes curvature algebra to Ford circles.
• The theorem catalogue now lists every declared entrypoint, conjectures included: 305 of 305.

What changed in admission since v0.2.0

What the receiver checks grew with what went wrong in practice (threat model).

• Statements are read as Lean writes them. Proofs by pattern matching, match inside a statement, let/have, dotted and primed names, and several namespaces per file used to be misread, silently.
• Triviality probes state each goal in its module's real context: the module's own imports, its open/variable/notation lines in order, its namespace, and no auto-bound implicits. A goal that cannot be stated from the baseline is reported not elaborated, with Lean's reason. Before, probes often ran on an auto-generalised statement.
• A statement screen in CI (tools/screen_statements.py) states every accepted entrypoint the way the probe would, and fails on any statement that cannot be stated for a reason other than naming its own module's definitions.
• A monthly kernel audit (lake check) replays the corpus and all of Mathlib through Lean's kernel, separately from admission. It also runs after every Lean/Mathlib upgrade.
• Upgrades: v4.35.0 was adopted by the automatic upgrade path, after a dry run on the release candidate found the one proof that needed changing a week early.

Data

The matching data release is corpus-v2: 110 submissions. Read its note on triviality-probe outcomes.

0.x: module and declaration names may still change between minor versions.