Kernel replays of sixteen Conjectures.io solutions

../

receipt_e0010_244ff2d0: Kernel replay of Conjectures.io record 244ff2d0 on Lean v4.34.1 from an empty environment, on 2026-10-14: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0014_adb53fba: Kernel replay of Conjectures.io record adb53fba on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0014_dce3d778: Kernel replay of Conjectures.io record dce3d778 on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0018_e93a2766: Kernel replay of Conjectures.io record e93a2766 on Lean v4.34.1 from an empty environment, on 2026-10-14: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0096_7ffd1c09: Kernel replay of Conjectures.io record 7ffd1c09 on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0108_8c083793: Kernel replay of Conjectures.io record 8c083793 on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0196_e73b95f7: Kernel replay of Conjectures.io record e73b95f7 on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0272_c3277f4a: Kernel replay of Conjectures.io record c3277f4a on Lean v4.34.1 from an empty environment, on 2026-10-14: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0354_815c1d5f: Kernel replay of Conjectures.io record 815c1d5f on Lean v4.34.1 from an empty environment, on 2026-10-14: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0416_51923647: Kernel replay of Conjectures.io record 51923647 on Lean v4.34.1 from an empty environment, on 2026-10-14: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0579_e4934265: Kernel replay of Conjectures.io record e4934265 on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0653_257ce6dd: Kernel replay of Conjectures.io record 257ce6dd on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0859_e060355f: Kernel replay of Conjectures.io record e060355f on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e0944_e7afff2c: Kernel replay of Conjectures.io record e7afff2c on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e1057_4b28b5fa: Kernel replay of Conjectures.io record 4b28b5fa on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

receipt_e1062_8d59a0af: Kernel replay of Conjectures.io record 8d59a0af on Lean v4.34.1 from an empty environment, on 2026-10-13: passed, with the axioms propext, Classical.choice and Quot.sound and the task's statement unchanged.

---

What a replay checks. For one record, replay.sh fetches the solution file by its URL and compares its SHA-256 with records.tsv. It reproduces the formal-conjectures commit the task pins: the base commit plus the audit patch that conjectures-tasks records, committed with the identity, date and message that conjectures-validator's scripts/pin_dependencies.sh uses. It ports that commit to the toolchain, takes the task bundle from conjectures-tasks and compares the bundle's files with its manifest. Solution.lean is the bundle's header, the solution file and the bundle's footer, with a proof-side port where records.tsv names one. After lake build Challenge Solution, Replay.lean collects every declaration Bounty.target depends on, replays them into an empty kernel environment, prints the axioms in that closure, and checks that the target's type, and every declaration its statement reaches, are identical in Challenge and Solution. Last, #print axioms Bounty.target runs on its own.

Files.

• replay.sh: the driver, replay.sh WORKDIR RECORD_ID. It reads its inputs from ../assets/, from Replay.lean, from lean/lean-toolchain and from public URLs: formal-conjectures, conjectures-tasks and conjectures-validator on GitHub, and the solution files on Conjectures.io. A changed file or bundle is reported, not refused.
• Replay.lean: the kernel replay, run as lake env lean --run Replay.lean Solution Challenge Bounty.target.
• records.tsv: per record, the solution file's SHA-256, the conjectures-tasks commit and bundle folder, the formal-conjectures commit the task pins and the one the file was built against, and its proof-side port with that diff's SHA-256.
• pins.tsv: per formal-conjectures commit, its base commit, the conjectures-tasks commit of its audit patch, and its port.
• ../assets/ports/: fc_<commit>.diff ports a pinned formal-conjectures commit to the toolchain (the Mathlib requirement, the toolchain file, a shared packages folder, and support files whose Mathlib API changed, as Conjectures.io's later port of formal-conjectures changes them).
• The proof-side port of a solution file, solution_<record>/port.diff under ../assets/, is held privately beside the solution file it quotes, for the seven records records.tsv names; the driver applies it where it is held and otherwise stops and names it.

Toolchain. The repository's lean/lean-toolchain, leanprover/lean4:v4.34.1, with Mathlib at the revision lean/lake-manifest.json pins. Conjectures.io checked the records on earlier toolchains: Lean v4.27.0 (Problem 10), v4.33.1 (fourteen records) and v4.35.0-rc2 (Problem 1057).

Results. All sixteen replays passed. The kernel accepted every closure from an empty environment, every target uses exactly propext, Classical.choice and Quot.sound, and every target's statement is identical to its task's. Seven files needed proof-side ports, for Problems 108, 354, 416, 579, 653, 859 and 1062, and none of them touches the target's statement. The source-type hash that Conjectures.io's inspector computes matches the task manifest for thirteen records. For Problems 10, 579 and 859 it differs on v4.34.1, where Mathlib elaborates the same statement text differently; the receipts say how. The statement check rests on the term comparison in Replay.lean, not on that hash.

Limits. Only Lean's own kernel was run, with no second kernel. The replays ran on 2026-10-13 and 2026-10-14 against the files whose SHA-256 the receipts name. The Problem 108 target alone is trivial, so its acceptance rests on the replayed lemma its receipt names. The finiteness of the Problem 944 witnesses rests on the claim page's reading of the file and was not rechecked here.