Audit final OEIS A147983 Lean module by DomTheDeveloper · Pull Request #76 · DomTheDeveloper/ProofPlaygrond

DomTheDeveloper · 2026-07-23T08:02:24Z

Audit branch neutralized after migration.

Authoritative artifact:

https://github.com/DomTheDeveloper/formal-conjectures/tree/a0c8858ce9b22166d0616931ea1fc996e335b03d/ProofArtifacts/OEIS/A147983

Authoritative submission PR:

DomTheDeveloper/formal-conjectures#185

github-actions · 2026-07-23T08:06:26Z

Superseded audit attempt; see the latest Final Chomp A147983 Lean audit v2 comment below.

github-actions · 2026-07-23T08:15:31Z

Superseded audit command (lake env lean lacked the project module mapping); see the latest v2 result.

github-actions · 2026-07-23T08:17:10Z

Superseded duplicate audit command; see the latest v2 result.

github-actions · 2026-07-23T08:17:14Z

Superseded audit command; see the latest audit for corrected DTD commit 8f81961ab4034852544a3443a82cdfad2212ad05.

github-actions · 2026-07-23T08:17:44Z

Superseded malformed reporter output; see the latest corrected-commit audit.

github-actions · 2026-07-23T08:18:49Z

Superseded pre-fix audit; it correctly identified the obsolete import. See the latest audit for corrected commit 8f81961ab4034852544a3443a82cdfad2212ad05.

github-actions · 2026-07-23T08:18:57Z

Superseded duplicate pre-fix audit; see the latest corrected-commit audit.

github-actions · 2026-07-23T08:19:12Z

Superseded pre-fix audit; see the latest audit for corrected commit 8f81961ab4034852544a3443a82cdfad2212ad05.

github-actions · 2026-07-23T08:19:13Z

Superseded duplicate pre-fix audit; see the latest corrected-commit audit.

github-actions · 2026-07-23T08:22:24Z

Superseded queued run from the deleted audit workflow; ignore.

github-actions · 2026-07-23T08:22:43Z

Superseded queued run from the deleted audit workflow; ignore.

github-actions · 2026-07-23T08:24:24Z

Final Chomp A147983 Lean audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
catalog module exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29990927361

Compiler tail

✔ [7961/7969] Built FormalConjecturesForMathlib.Computability.Encoding (1.5s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.1s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.4s)
✔ [7964/7972] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.3s)
✔ [7965/7972] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.1s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.3s)
✔ [7967/7974] Built FormalConjecturesForMathlib.Data.Nat.Init (1.0s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (1.8s)
✔ [7969/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (2.3s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Data.Nat.Full (1.9s)
✔ [7971/7977] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (1.6s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.1s)
✔ [7973/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (3.1s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.4s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (2.6s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.1s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.3s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Set.Interval (1.3s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Real.Constants (2.1s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (2.9s)
✔ [7981/7987] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.5s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.4s)
✔ [7983/7989] Built FormalConjecturesForMathlib.Data.Set.Triplewise (1.9s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.4s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (1.6s)
✔ [7986/7990] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (1.7s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.2s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Geometry.Metric (1.4s)
✔ [7989/7995] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.1s)
✔ [7990/7996] Built FormalConjecturesForMathlib.Data.Set.Density (4.1s)
✔ [7991/7998] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (1.8s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (2.4s)
✔ [7993/8000] Built FormalConjecturesForMathlib.NumberTheory.Amicable (1.6s)
✔ [7994/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (1.8s)
✔ [7995/8002] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.5s)
✔ [7996/8003] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (1.5s)
✔ [7997/8003] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (2.6s)
✔ [7998/8004] Built FormalConjecturesForMathlib.Geometry.«2d» (7.3s)
✔ [7999/8005] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (1.7s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (1.5s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (4.7s)
✔ [8002/8008] Built FormalConjecturesForMathlib.NumberTheory.Divisors (1.5s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (1.9s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (1.9s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (1.5s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (1.0s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.3s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.3s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.Primitive (1.6s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.1s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (2.8s)
✔ [8012/8018] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.4s)
✔ [8013/8020] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (2.5s)
✔ [8014/8020] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.4s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (1.6s)
✔ [8016/8022] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.4s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.4s)
✔ [8018/8026] Built FormalConjecturesForMathlib.Topology.Discrete (1.3s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.4s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (261ms)
✔ [8021/8033] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.4s)
✔ [8022/8033] Built FormalConjecturesUtil.Answer (870ms)
✔ [8023/8037] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.3s)
✔ [8025/8040] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.4s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (331ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (558ms)
✔ [8028/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (844ms)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (609ms)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (1.4s)
✔ [8031/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (590ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (553ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (1.7s)
✔ [8034/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.2s)
✔ [8035/8040] Built FormalConjecturesForMathlib (3.0s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.3s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.4s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.AMSLinter (1.3s)
✔ [8039/8040] Built FormalConjecturesUtil (2.8s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (3.8s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:24:37Z

Final Chomp A147983 Lean audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
catalog module exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29990938101

Compiler tail

✔ [7961/7969] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.1s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Computability.Encoding (1.4s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.5s)
✔ [7964/7971] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.3s)
✔ [7965/7972] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.3s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.1s)
✔ [7967/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (1.7s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Init (1.1s)
✔ [7969/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (2.3s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Data.Nat.Full (1.9s)
✔ [7971/7977] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (1.6s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.1s)
✔ [7973/7979] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.3s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (2.8s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (3.4s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.0s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.3s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Set.Interval (1.3s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Real.Constants (2.1s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (2.0s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.5s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.5s)
✔ [7983/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (1.8s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.3s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (1.6s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (1.7s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.5s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.2s)
✔ [7989/7995] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.2s)
✔ [7990/7996] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (1.9s)
✔ [7991/7999] Built FormalConjecturesForMathlib.Data.Set.Density (4.2s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (2.6s)
✔ [7993/8000] Built FormalConjecturesForMathlib.NumberTheory.Amicable (1.5s)
✔ [7994/8001] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.1s)
✔ [7995/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (1.8s)
✔ [7996/8002] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (2.5s)
✔ [7997/8004] Built FormalConjecturesForMathlib.Geometry.«2d» (6.4s)
✔ [7998/8004] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (2.7s)
✔ [7999/8005] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (1.5s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.Divisors (1.5s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (1.6s)
✔ [8002/8008] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (5.1s)
✔ [8003/8010] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (1.9s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (1.5s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (1.9s)
✔ [8006/8013] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.0s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.3s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.3s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.2s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (2.7s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (1.6s)
✔ [8012/8018] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.5s)
✔ [8013/8019] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (2.5s)
✔ [8014/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (1.6s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.3s)
✔ [8016/8022] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.4s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.4s)
✔ [8018/8026] Built FormalConjecturesForMathlib.Topology.Discrete (1.3s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.3s)
✔ [8020/8026] Built FormalConjecturesUtil.Answer.Syntax (259ms)
✔ [8021/8030] Built FormalConjecturesUtil.Answer (901ms)
✔ [8022/8036] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.4s)
✔ [8023/8036] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.3s)
✔ [8025/8040] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.4s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (337ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (608ms)
✔ [8028/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (870ms)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (619ms)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (1.4s)
✔ [8031/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (632ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (539ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (1.6s)
✔ [8034/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.3s)
✔ [8035/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.3s)
✔ [8036/8040] Built FormalConjecturesForMathlib (4.1s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.4s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.AMSLinter (1.3s)
✔ [8039/8040] Built FormalConjecturesUtil (2.9s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (3.9s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:32:57Z

Final Chomp A147983 Lean audit: FAIL

exact DTD commit: 573502ae849f8028d1aceeb09a6e339b4a167816
catalog module compile: failure
no-sorryAx reduction-lemma audit: skipped
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29991432973

Compiler tail

FormalConjectures/OEIS/147983.lean:17:0: error: unknown module prefix 'FormalConjectures'

No directory 'FormalConjectures' or file 'FormalConjectures.olean' in the search path entries:
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/Cli/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/batteries/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/Qq/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/aesop/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/importGraph/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/plausible/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/mathlib/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/build/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean

github-actions · 2026-07-23T08:33:01Z

Final Chomp A147983 Lean audit v2: FAIL

exact DTD commit: 573502ae849f8028d1aceeb09a6e339b4a167816
catalog module exit code: 1
reduction-lemma axiom audit exit code: 125
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29991432937

Compiler tail

FormalConjectures/OEIS/147983.lean:17:0: error: unknown module prefix 'FormalConjectures'

No directory 'FormalConjectures' or file 'FormalConjectures.olean' in the search path entries:
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/Cli/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/batteries/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/Qq/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/aesop/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/importGraph/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/plausible/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/packages/mathlib/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/formal-conjectures/.lake/build/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean

github-actions · 2026-07-23T08:46:12Z

Final Chomp A147983 Lean audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
catalog module exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29991978471

Compiler tail

✔ [7961/7969] Built FormalConjecturesForMathlib.Computability.Encoding (1.9s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.8s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.7s)
✔ [7964/7972] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.9s)
✔ [7965/7973] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.4s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.7s)
✔ [7967/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (2.2s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Init (1.4s)
✔ [7969/7976] Built FormalConjecturesForMathlib.Data.Nat.Full (2.3s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (3.1s)
✔ [7971/7978] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (1.0s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.7s)
✔ [7973/7979] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.7s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (4.4s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.8s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (3.6s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.8s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Set.Interval (1.7s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Real.Constants (3.1s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (3.0s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.9s)
✔ [7982/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.8s)
✔ [7983/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (2.1s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (2.5s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.8s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (2.2s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.8s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.8s)
✔ [7989/7996] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.7s)
✔ [7990/7996] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (2.3s)
✔ [7991/7998] Built FormalConjecturesForMathlib.Data.Set.Density (5.7s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (3.8s)
✔ [7993/8000] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.0s)
✔ [7994/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (2.2s)
✔ [7995/8001] Built FormalConjecturesForMathlib.NumberTheory.Amicable (1.0s)
✔ [7996/8002] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (2.0s)
✔ [7997/8003] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (2.4s)
✔ [7998/8004] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (2.8s)
✔ [7999/8005] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (3.0s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.Divisors (2.7s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (7.0s)
✔ [8002/8008] Built FormalConjecturesForMathlib.Geometry.«2d» (9.7s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (2.7s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (2.5s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (2.0s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.7s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.8s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.7s)
✔ [8009/8016] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (3.8s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.5s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (2.1s)
✔ [8012/8019] Built FormalConjecturesForMathlib.Probability.FiniteMethod (2.1s)
✔ [8013/8019] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.8s)
✔ [8014/8020] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (2.2s)
✔ [8015/8021] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (3.6s)
✔ [8016/8024] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.9s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.9s)
✔ [8018/8024] Built FormalConjecturesForMathlib.Topology.Discrete (1.8s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.9s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (336ms)
✔ [8021/8030] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.7s)
✔ [8022/8033] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.9s)
✔ [8023/8036] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.9s)
✔ [8024/8037] Built FormalConjecturesUtil.Answer (1.2s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (464ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (795ms)
✔ [8028/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (983ms)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (1.2s)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (2.1s)
✔ [8031/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (811ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (798ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (2.3s)
✔ [8034/8040] Built FormalConjecturesForMathlib (5.2s)
✔ [8035/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.8s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.9s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.5s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.AMSLinter (2.6s)
✔ [8039/8040] Built FormalConjecturesUtil (3.8s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (4.9s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:46:44Z

Final Chomp A147983 audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
fatal-warning module build exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29992018592

Compiler tail

✔ [7961/7970] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.7s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Computability.Encoding (1.8s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.8s)
✔ [7964/7971] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.6s)
✔ [7965/7972] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.3s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.6s)
✔ [7967/7974] Built FormalConjecturesForMathlib.Data.Nat.Init (1.3s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (2.0s)
✔ [7969/7976] Built FormalConjecturesForMathlib.Data.Nat.Full (2.3s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (2.9s)
✔ [7971/7978] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (1.0s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.4s)
✔ [7973/7979] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.5s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.5s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (3.0s)
✔ [7976/7981] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (3.5s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.7s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Real.Constants (2.9s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Set.Interval (1.6s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (3.7s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.9s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.8s)
✔ [7983/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (1.0s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.6s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (2.4s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (1.0s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.8s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.5s)
✔ [7989/7996] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.6s)
✔ [7990/7996] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (2.2s)
✔ [7991/7999] Built FormalConjecturesForMathlib.Data.Set.Density (5.3s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (3.2s)
✔ [7993/8000] Built FormalConjecturesForMathlib.NumberTheory.Amicable (2.1s)
✔ [7994/8001] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.6s)
✔ [7995/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (2.2s)
✔ [7996/8002] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (2.6s)
✔ [7997/8003] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (3.2s)
✔ [7998/8004] Built FormalConjecturesForMathlib.Geometry.«2d» (8.7s)
✔ [7999/8005] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (2.0s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (1.9s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Divisors (1.8s)
✔ [8002/8008] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (6.5s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (2.4s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (2.3s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (1.9s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.5s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.6s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.6s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (3.4s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.4s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (1.0s)
✔ [8012/8018] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.8s)
✔ [8013/8019] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (3.1s)
✔ [8014/8020] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (2.1s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.7s)
✔ [8016/8022] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.7s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.6s)
✔ [8018/8024] Built FormalConjecturesForMathlib.Topology.Discrete (1.6s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.6s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (333ms)
✔ [8021/8030] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.7s)
✔ [8022/8033] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.5s)
✔ [8023/8033] Built FormalConjecturesUtil.Answer (1.1s)
✔ [8025/8040] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.9s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (429ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (716ms)
✔ [8028/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (1.1s)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (726ms)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (1.9s)
✔ [8031/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (697ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (767ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (2.2s)
✔ [8034/8040] Built FormalConjecturesForMathlib (4.0s)
✔ [8035/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.6s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.7s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.AMSLinter (2.2s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.1s)
✔ [8039/8040] Built FormalConjecturesUtil (3.6s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (4.6s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:47:09Z

Final Chomp A147983 fatal-warning audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
fatal-warning module build exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29992031531

Compiler tail

✔ [7961/7969] Built FormalConjecturesForMathlib.Computability.Encoding (1.9s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.9s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.0s)
✔ [7964/7972] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.8s)
✔ [7965/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.7s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.4s)
✔ [7967/7974] Built FormalConjecturesForMathlib.Data.Nat.Init (1.3s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (2.2s)
✔ [7969/7976] Built FormalConjecturesForMathlib.Data.Nat.Full (2.7s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (3.2s)
✔ [7971/7977] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (1.0s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.5s)
✔ [7973/7979] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.8s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.8s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (4.3s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (3.4s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.7s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Set.Interval (1.7s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Real.Constants (2.9s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (3.8s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.9s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.9s)
✔ [7983/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.8s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (2.7s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (1.0s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (2.4s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.9s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.6s)
✔ [7989/7996] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.9s)
✔ [7990/7996] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (2.3s)
✔ [7991/7998] Built FormalConjecturesForMathlib.Data.Set.Density (5.5s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (3.8s)
✔ [7993/8000] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (2.4s)
✔ [7994/8001] Built FormalConjecturesForMathlib.NumberTheory.Amicable (2.1s)
✔ [7995/8002] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.9s)
✔ [7996/8003] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (2.7s)
✔ [7997/8003] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (3.3s)
✔ [7998/8004] Built FormalConjecturesForMathlib.Geometry.«2d» (9.2s)
✔ [7999/8005] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (2.3s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (2.0s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Divisors (1.9s)
✔ [8002/8008] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (6.5s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (2.5s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (2.5s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (2.0s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.7s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.7s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.7s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (3.6s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.6s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (2.1s)
✔ [8012/8019] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (3.3s)
✔ [8013/8019] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.9s)
✔ [8014/8020] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.8s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (2.0s)
✔ [8016/8024] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.8s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.7s)
✔ [8018/8024] Built FormalConjecturesForMathlib.Topology.Discrete (1.8s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.8s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (350ms)
✔ [8021/8037] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.8s)
✔ [8022/8037] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.7s)
✔ [8023/8037] Built FormalConjecturesUtil.Answer (1.2s)
✔ [8025/8040] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.9s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (468ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (756ms)
✔ [8028/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (1.1s)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (841ms)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (1.0s)
✔ [8031/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (748ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (694ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (2.1s)
✔ [8034/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.7s)
✔ [8035/8040] Built FormalConjecturesForMathlib (5.3s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.8s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.9s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.AMSLinter (1.7s)
✔ [8039/8040] Built FormalConjecturesUtil (3.9s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (5.0s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:49:16Z

Final Chomp A147983 fatal-warning audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
fatal-warning module build exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29992206383

Compiler tail

✔ [7961/7969] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.8s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Computability.Encoding (1.9s)
✔ [7963/7971] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.9s)
✔ [7964/7972] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.7s)
✔ [7965/7972] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.4s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.8s)
✔ [7967/7975] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (2.1s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Init (1.3s)
✔ [7969/7976] Built FormalConjecturesForMathlib.Data.Nat.Full (2.4s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (3.2s)
✔ [7971/7978] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (2.2s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.5s)
✔ [7973/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.7s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.7s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (4.4s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (3.4s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.8s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Real.Constants (2.9s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Set.Interval (1.8s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (3.8s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.9s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.9s)
✔ [7983/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.7s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.ZMod.Fp (2.0s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (2.5s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (2.3s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.9s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.8s)
✔ [7989/7996] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.5s)
✔ [7990/7997] Built FormalConjecturesForMathlib.Data.Set.Density (5.4s)
✔ [7991/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (3.4s)
✔ [7992/7999] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (2.6s)
✔ [7993/8000] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (2.0s)
✔ [7994/8001] Built FormalConjecturesForMathlib.NumberTheory.Amicable (1.9s)
✔ [7995/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (2.0s)
✔ [7996/8002] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (1.9s)
✔ [7997/8003] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (2.2s)
✔ [7998/8004] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (2.5s)
✔ [7999/8005] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (3.0s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.Divisors (2.0s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (6.4s)
✔ [8002/8008] Built FormalConjecturesForMathlib.Geometry.«2d» (9.5s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (2.7s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (2.5s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (1.0s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.6s)
✔ [8007/8014] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.7s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.7s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (3.6s)
✔ [8010/8016] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.5s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (2.0s)
✔ [8012/8019] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (3.2s)
✔ [8013/8019] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.9s)
✔ [8014/8020] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (2.1s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.7s)
✔ [8016/8024] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.9s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.8s)
✔ [8018/8024] Built FormalConjecturesForMathlib.Topology.Discrete (1.7s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.7s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (358ms)
✔ [8021/8030] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.8s)
✔ [8022/8033] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.9s)
✔ [8023/8036] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.6s)
✔ [8024/8036] Built FormalConjecturesUtil.Answer (1.2s)
✔ [8025/8037] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (427ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (795ms)
✔ [8028/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (870ms)
✔ [8029/8040] Built FormalConjecturesUtil.Attributes.AMS (2.1s)
✔ [8030/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (1.1s)
✔ [8031/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (770ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (764ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (2.2s)
✔ [8034/8040] Built FormalConjecturesForMathlib (4.9s)
✔ [8035/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.8s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.7s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.AMSLinter (2.4s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.6s)
✔ [8039/8040] Built FormalConjecturesUtil (3.5s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (4.6s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

github-actions · 2026-07-23T08:55:03Z

Final Chomp A147983 fatal-warning audit: PASS

exact DTD commit: 8f81961ab4034852544a3443a82cdfad2212ad05
fatal-warning module build exit code: 0
reduction-lemma axiom audit exit code: 0
workflow run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/29992559940

Compiler tail

✔ [7961/7970] Built FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph (2.9s)
✔ [7962/7970] Built FormalConjecturesForMathlib.Computability.Encoding (1.9s)
✔ [7963/7972] Built FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine (1.9s)
✔ [7964/7972] Built FormalConjecturesForMathlib.Data.Finset.Powerset (1.7s)
✔ [7965/7972] Built FormalConjecturesForMathlib.Data.Int.IntermediateValue (1.4s)
✔ [7966/7973] Built FormalConjecturesForMathlib.Data.Finset.ReciprocalSum (1.7s)
✔ [7967/7974] Built FormalConjecturesForMathlib.Data.Nat.Factorization.Basic (2.2s)
✔ [7968/7975] Built FormalConjecturesForMathlib.Data.Nat.Init (1.4s)
✔ [7969/7977] Built FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers (3.2s)
✔ [7970/7977] Built FormalConjecturesForMathlib.Data.Nat.Full (2.5s)
✔ [7971/7978] Built FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac (2.2s)
✔ [7972/7978] Built FormalConjecturesForMathlib.Data.Nat.Prime.Composite (1.5s)
✔ [7973/7979] Built FormalConjecturesForMathlib.Data.Nat.Prime.Defs (2.6s)
✔ [7974/7980] Built FormalConjecturesForMathlib.Data.Nat.Prime.Finset (1.8s)
✔ [7975/7980] Built FormalConjecturesForMathlib.Data.Nat.PerfectPower (4.4s)
✔ [7976/7982] Built FormalConjecturesForMathlib.Computability.TuringMachine.Notation (3.7s)
✔ [7977/7984] Built FormalConjecturesForMathlib.Data.Real.NearestInt (1.8s)
✔ [7978/7985] Built FormalConjecturesForMathlib.Data.Real.Constants (3.1s)
✔ [7979/7986] Built FormalConjecturesForMathlib.Data.Set.Interval (1.8s)
✔ [7980/7987] Built FormalConjecturesForMathlib.Data.Nat.Squarefree (4.1s)
✔ [7981/7988] Built FormalConjecturesForMathlib.Order.Interval.Finset.Basic (1.9s)
✔ [7982/7989] Built FormalConjecturesForMathlib.Order.Interval.Finset.Nat (1.8s)
✔ [7983/7989] Built FormalConjecturesForMathlib.Data.ZMod.Fp (1.0s)
✔ [7984/7990] Built FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet (1.9s)
✔ [7985/7990] Built FormalConjecturesForMathlib.Data.Set.Triplewise (2.7s)
✔ [7986/7993] Built FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs (2.3s)
✔ [7987/7994] Built FormalConjecturesForMathlib.Geometry.Metric (1.0s)
✔ [7988/7995] Built FormalConjecturesForMathlib.Geometry.Euclidean (2.9s)
✔ [7989/7996] Built FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate (1.7s)
✔ [7990/7997] Built FormalConjecturesForMathlib.Data.Set.Density (5.7s)
✔ [7991/7998] Built FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic (2.7s)
✔ [7992/7999] Built FormalConjecturesForMathlib.Geometry.«3d» (3.6s)
✔ [7993/8000] Built FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup (3.0s)
✔ [7994/8000] Built FormalConjecturesForMathlib.NumberTheory.Amicable (1.9s)
✔ [7995/8001] Built FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete (2.2s)
✔ [7996/8002] Built FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes (1.9s)
✔ [7997/8003] Built FormalConjecturesForMathlib.NumberTheory.CoveringSystem (2.1s)
✔ [7998/8004] Built FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup (2.6s)
✔ [7999/8005] Built FormalConjecturesForMathlib.NumberTheory.Divisors (3.0s)
✔ [8000/8006] Built FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic (3.3s)
✔ [8001/8007] Built FormalConjecturesForMathlib.NumberTheory.Carmichael (6.6s)
✔ [8002/8008] Built FormalConjecturesForMathlib.Geometry.«2d» (9.6s)
✔ [8003/8009] Built FormalConjecturesForMathlib.NumberTheory.Lacunary (2.5s)
✔ [8004/8010] Built FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic (2.6s)
✔ [8005/8011] Built FormalConjecturesForMathlib.NumberTheory.NormalNumber (1.0s)
✔ [8006/8012] Built FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic (2.6s)
✔ [8007/8013] Built FormalConjecturesForMathlib.NumberTheory.PracticalNumbers (1.8s)
✔ [8008/8014] Built FormalConjecturesForMathlib.NumberTheory.PrimeGap (1.6s)
✔ [8009/8015] Built FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber (1.6s)
✔ [8010/8017] Built FormalConjecturesForMathlib.NumberTheory.PisotNumber (3.7s)
✔ [8011/8017] Built FormalConjecturesForMathlib.NumberTheory.Primitive (2.1s)
✔ [8012/8018] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum (1.7s)
✔ [8013/8019] Built FormalConjecturesForMathlib.Probability.FiniteMethod (1.9s)
✔ [8014/8020] Built FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes (3.5s)
✔ [8015/8021] Built FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic (2.1s)
✔ [8016/8024] Built FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph (1.8s)
✔ [8017/8024] Built FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract (1.8s)
✔ [8018/8024] Built FormalConjecturesForMathlib.Topology.Discrete (1.7s)
✔ [8019/8026] Built FormalConjecturesForMathlib.Topology.GDelta (1.7s)
✔ [8020/8029] Built FormalConjecturesUtil.Answer.Syntax (370ms)
✔ [8021/8030] Built FormalConjecturesForMathlib.Topology.Homogeneous (1.6s)
✔ [8022/8037] Built FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension (1.9s)
✔ [8023/8037] Built FormalConjecturesUtil.Answer (1.2s)
✔ [8025/8040] Built FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated (1.0s)
✔ [8026/8040] Built FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util (480ms)
✔ [8027/8040] Built FormalConjecturesUtil.Linters.CopyrightLinter (777ms)
✔ [8028/8040] Built FormalConjecturesUtil.Linters.ModuleDocstringLinter (1.2s)
✔ [8029/8040] Built FormalConjecturesUtil.Linters.NamespaceLinter (814ms)
✔ [8030/8040] Built FormalConjecturesUtil.Attributes.AMS (1.9s)
✔ [8031/8040] Built FormalConjecturesForMathlib.Tactic.Linter.Term (815ms)
✔ [8032/8040] Built FormalConjecturesUtil.Linters.ExistsImplicationLinter (541ms)
✔ [8033/8040] Built FormalConjecturesUtil.Attributes.Basic (2.3s)
✔ [8034/8040] Built FormalConjecturesUtil.Linters.CategoryDocstringLinter (1.7s)
✔ [8035/8040] Built FormalConjecturesForMathlib (5.4s)
✔ [8036/8040] Built FormalConjecturesUtil.Linters.AnswerLinter (1.8s)
✔ [8037/8040] Built FormalConjecturesUtil.Linters.CategoryLinter (1.9s)
✔ [8038/8040] Built FormalConjecturesUtil.Linters.AMSLinter (1.8s)
✔ [8039/8040] Built FormalConjecturesUtil (3.6s)
✔ [8040/8040] Built FormalConjectures.OEIS.«147983» (4.8s)
Build completed successfully (8040 jobs).

Axiom audit output

'OeisA147983.child₁_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
ChompA147983Audit.lean:3:0: warning: This file has no module docstring (`/-! ... -/`). Add one after the imports to document the file.

Note: This linter can be disabled with `set_option linter.style.moduleDocstring false`
'OeisA147983.child₂_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.child₃_is_legal_move' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA147983.candidate_children_pairwise_distinct' does not depend on any axioms
'OeisA147983.three_openings_of_p_positions' depends on axioms: [propext, Classical.choice, Quot.sound]

DomTheDeveloper closed this Jul 23, 2026

DomTheDeveloper reopened this Jul 23, 2026

DomTheDeveloper closed this Jul 23, 2026

DomTheDeveloper force-pushed the audit/chomp-a147983-final-lean branch from c6cf52f to 7486225 Compare July 23, 2026 09:02

Conversation

DomTheDeveloper commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026 • edited by DomTheDeveloper Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 Lean audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 Lean audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 Lean audit: FAIL

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 Lean audit v2: FAIL

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 Lean audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 fatal-warning audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 fatal-warning audit: PASS

Uh oh!

github-actions Bot commented Jul 23, 2026

Final Chomp A147983 fatal-warning audit: PASS

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

DomTheDeveloper commented Jul 23, 2026 •

edited

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading

github-actions Bot commented Jul 23, 2026 •

edited by DomTheDeveloper

Loading