Solution: six distances from the E2 diameter-heptagon pattern - #359
Draft
lyfar wants to merge 28 commits into
Draft
Solution: six distances from the E2 diameter-heptagon pattern#359lyfar wants to merge 28 commits into
lyfar wants to merge 28 commits into
Conversation
Source DOI: 10.11650/tjm.18.2014.4030 Certificates: https://github.com/lyfar/erdos132-wei-certificates Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 334 maxHeartbeats units across 14 files (3,325 added LOC). Sum of Count-heartbeats wall-clock total: 105.92 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Erdos132WeiE2.Algebra.BezoutGenerated |
19.00 s |
LeanPool.Erdos132WeiE2.Geometry.Parametrization |
15.00 s |
LeanPool.Erdos132WeiE2.Algebra.Exclusions |
10.00 s |
LeanPool.Erdos132WeiE2.Geometry.Star |
9.70 s |
LeanPool.Erdos132WeiE2.Counting.Endgame |
8.80 s |
Challenge.WeiLiCongGao |
6.70 s |
LeanPool.Erdos132WeiE2.Algebra.Ranges |
6.50 s |
LeanPool.Erdos132WeiE2.Geometry.Basic |
6.20 s |
LeanPool.Erdos132WeiE2.Algebra.G10 |
5.80 s |
LeanPool.Erdos132WeiE2.Algebra.TrigSigns |
4.70 s |
LeanPool.Erdos132WeiE2.Algebra.TanExpressions |
3.60 s |
LeanPool.Erdos132WeiE2.Counting.Assembly |
3.10 s |
Per-file `lean --profile` output
Challenge/WeiLiCongGao.lean
import took 1.43s
Challenge/WeiLiCongGao.lean:42:8: warning: declaration uses `sorry`
cumulative profiling times:
attribute application 0.0113ms
elaboration 12.9ms
fix level params 0.0521ms
import 1.43s
initialization 29.3ms
instantiate metavars 0.0412ms
interpretation 188ms
let-to-have transformation 0.0603ms
linting 1.27ms
module linting 0.00133ms
overlappingInstancesLinter 0.99ms
parsing 1.69ms
process pre-definitions 0.294ms
share common exprs 0.357ms
tacticAnalysis 3.88ms
type checking 1.39ms
typeclass inference 8.23ms
real 2.30
user 1.30
sys 1.03
LeanPool/Erdos132WeiE2.lean
import took 1.72s
cumulative profiling times:
elaboration 0.319ms
import 1.72s
initialization 28.1ms
interpretation 191ms
linting 0.33ms
module linting 0.00125ms
overlappingInstancesLinter 0.181ms
parsing 0.0281ms
tacticAnalysis 0.799ms
real 2.60
user 1.45
sys 1.17
LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean
import took 849ms
elaboration took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 895ms
ring took 233ms
share common exprs took 114ms
type checking took 443ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 878ms
ring took 106ms
type checking took 238ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 748ms
ring took 124ms
type checking took 224ms
cumulative profiling times:
attribute application 0.106ms
congr simp thm 1.64ms
elaboration 651ms
fix level params 17.1ms
import 849ms
initialization 29.7ms
instantiate metavars 2.45ms
interpretation 3.06s
let-to-have transformation 0.448ms
linting 17.5ms
module linting 0.00147ms
norm_num 2.75s
overlappingInstancesLinter 3.75ms
parsing 18.9ms
process pre-definitions 155ms
ring 464ms
share common exprs 234ms
tactic execution 1.27ms
tacticAnalysis 58.4ms
type checking 941ms
typeclass inference 5.74s
real 9.68
user 14.86
sys 0.76
LeanPool/Erdos132WeiE2/Algebra/Exclusions.lean
import took 1.27s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 304ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 607ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 546ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.42s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.37s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 181ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.5s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 123ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.47s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.24s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.07s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 111ms
cumulative profiling times:
attribute application 0.144ms
compilation (IR) 0.383ms
compilation (LCNF base) 14ms
compilation (LCNF impure) 1.53ms
compilation (LCNF mono) 5.47ms
congr simp thm 4.81ms
dsimp 3.69ms
elaboration 246ms
fix level params 5.1ms
import 1.27s
initialization 29.3ms
instantiate metavars 16.9ms
interpretation 13.7s
let-to-have transformation 0.394ms
linting 135ms
module linting 0.00118ms
norm_num 368ms
overlappingInstancesLinter 4.37ms
parsing 17.8ms
process pre-definitions 44ms
ring 296ms
share common exprs 134ms
simp 56.9ms
tactic execution 390ms
tacticAnalysis 58.9ms
type checking 312ms
typeclass inference 2.75s
real 7.40
user 19.53
sys 0.98
LeanPool/Erdos132WeiE2/Algebra/G10.lean
import took 1.27s
cumulative profiling times:
attribute application 0.0236ms
congr simp thm 2.13ms
elaboration 51.4ms
fix level params 1.07ms
import 1.27s
initialization 29.3ms
instantiate metavars 1.74ms
interpretation 847ms
let-to-have transformation 0.0756ms
linting 18ms
module linting 0.00158ms
norm_num 312ms
overlappingInstancesLinter 1.47ms
parsing 6.27ms
process pre-definitions 12.3ms
ring 93.4ms
share common exprs 23.7ms
simp 16.5ms
tactic execution 131ms
tacticAnalysis 13.7ms
type checking 48.9ms
typeclass inference 451ms
real 3.85
user 3.03
sys 0.93
LeanPool/Erdos132WeiE2/Algebra/Ranges.lean
import took 1.25s
cumulative profiling times:
attribute application 0.0583ms
congr simp thm 0.267ms
elaboration 38.2ms
fix level params 0.417ms
import 1.25s
initialization 40.5ms
instantiate metavars 0.459ms
interpretation 280ms
let-to-have transformation 0.122ms
linting 10.2ms
module linting 0.0013ms
norm_num 25.3ms
overlappingInstancesLinter 1.7ms
parsing 3.2ms
process pre-definitions 3.01ms
ring 21.3ms
share common exprs 4.82ms
simp 1.04ms
tactic execution 8.58ms
tacticAnalysis 12.8ms
type checking 16.6ms
typeclass inference 69.1ms
real 2.31
user 1.47
sys 0.95
LeanPool/Erdos132WeiE2/Algebra/TanExpressions.lean
import took 1.25s
cumulative profiling times:
attribute application 0.0748ms
congr simp thm 0.531ms
elaboration 30.7ms
fix level params 0.63ms
import 1.25s
initialization 28.8ms
instantiate metavars 0.477ms
interpretation 350ms
let-to-have transformation 0.107ms
linting 6.71ms
module linting 0.00133ms
norm_num 43.5ms
overlappingInstancesLinter 1.9ms
parsing 3.93ms
process pre-definitions 4.25ms
ring 41.6ms
share common exprs 6.66ms
simp 1.98ms
tactic execution 33ms
tacticAnalysis 13.8ms
type checking 44.5ms
typeclass inference 148ms
real 2.31
user 1.68
sys 0.94
LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean
import took 1.25s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 147ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 126ms
cumulative profiling times:
attribute application 0.19ms
congr simp thm 0.897ms
elaboration 118ms
fix level params 1.93ms
import 1.25s
initialization 36.7ms
instantiate metavars 1.96ms
interpretation 772ms
let-to-have transformation 0.358ms
linting 22ms
module linting 0.00153ms
norm_num 122ms
overlappingInstancesLinter 3.72ms
parsing 10.5ms
process pre-definitions 13.4ms
ring 109ms
share common exprs 25.4ms
simp 5.17ms
tactic execution 83.3ms
tacticAnalysis 38.6ms
type checking 112ms
typeclass inference 559ms
real 2.60
user 2.98
sys 0.91
LeanPool/Erdos132WeiE2/Counting/Assembly.lean
import took 1.69s
cumulative profiling times:
attribute application 0.0119ms
congr simp thm 1.63ms
elaboration 32.4ms
fix level params 0.357ms
import 1.69s
initialization 28.6ms
instantiate metavars 0.821ms
interpretation 560ms
let-to-have transformation 0.0871ms
linting 24.5ms
module linting 0.00124ms
norm_num 83.2ms
overlappingInstancesLinter 2.09ms
parsing 11.5ms
process pre-definitions 3.92ms
ring 15.4ms
share common exprs 4.41ms
simp 16.6ms
tactic execution 134ms
tacticAnalysis 24.7ms
type checking 15.2ms
typeclass inference 187ms
real 3.46
user 2.33
sys 1.16
LeanPool/Erdos132WeiE2/Counting/Endgame.lean
import took 1.65s
cumulative profiling times:
attribute application 0.0122ms
congr simp thm 5.21ms
elaboration 11.4ms
fix level params 0.307ms
import 1.65s
initialization 29.5ms
instantiate metavars 1.37ms
interpretation 428ms
let-to-have transformation 0.0247ms
linting 12.9ms
module linting 0.00141ms
norm_num 2.02ms
overlappingInstancesLinter 0.821ms
parsing 3.89ms
process pre-definitions 2.91ms
ring 32.9ms
share common exprs 6.52ms
simp 102ms
tactic execution 57.5ms
tacticAnalysis 11.3ms
type checking 21.5ms
typeclass inference 82ms
real 3.10
user 1.98
sys 1.15
LeanPool/Erdos132WeiE2/Geometry/Basic.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 226ms
cumulative profiling times:
attribute application 0.15ms
blocked (unaccounted) 0.965ms
compilation (IR) 0.0324ms
compilation (LCNF base) 0.566ms
compilation (LCNF impure) 0.152ms
compilation (LCNF mono) 0.22ms
congr simp thm 0.866ms
elaboration 67ms
fix level params 1.21ms
import 1.45s
initialization 36.9ms
instantiate metavars 11.6ms
interpretation 786ms
let-to-have transformation 0.327ms
linting 16.9ms
module linting 0.00128ms
norm_num 1.88ms
overlappingInstancesLinter 3.46ms
parsing 11.1ms
process pre-definitions 21.3ms
ring 20.8ms
share common exprs 10.3ms
simp 78.6ms
tactic execution 219ms
tacticAnalysis 28.4ms
type checking 203ms
typeclass inference 497ms
real 3.20
user 3.03
sys 1.05
LeanPool/Erdos132WeiE2/Geometry/Parametrization.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 502ms
simp took 697ms
simp took 334ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 118ms
simp took 106ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 209ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.38s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.34s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 718ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.82s
cumulative profiling times:
attribute application 1.2ms
blocked (unaccounted) 1.63s
compilation (IR) 0.0503ms
compilation (LCNF base) 0.799ms
compilation (LCNF impure) 0.271ms
compilation (LCNF mono) 0.536ms
congr simp thm 12.7ms
elaboration 595ms
fix level params 8.12ms
import 1.45s
initialization 29.7ms
instantiate metavars 16.7ms
interpretation 8.31s
let-to-have transformation 1.25ms
linting 169ms
module linting 0.00135ms
norm_num 599ms
overlappingInstancesLinter 16.6ms
parsing 97ms
process pre-definitions 80.2ms
ring 469ms
share common exprs 135ms
simp 2.06s
tactic execution 2.01s
tacticAnalysis 246ms
type checking 1.08s
typeclass inference 4.83s
real 9.82
user 21.37
sys 1.13
LeanPool/Erdos132WeiE2/Geometry/Star.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 670ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 614ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 846ms
simp took 413ms
simp took 354ms
simp took 362ms
simp took 353ms
cumulative profiling times:
attribute application 0.282ms
congr simp thm 52.3ms
elaboration 195ms
fix level params 6.34ms
import 1.45s
initialization 29.1ms
instantiate metavars 47.7ms
interpretation 3.73s
let-to-have transformation 0.528ms
linting 101ms
module linting 0.00169ms
norm_num 8.18ms
overlappingInstancesLinter 8.08ms
parsing 55.8ms
process pre-definitions 107ms
ring 159ms
share common exprs 78.6ms
simp 5.17s
tactic execution 1.44s
tacticAnalysis 127ms
type checking 443ms
typeclass inference 3.14s
real 7.27
user 15.84
sys 1.12
Solution/WeiLiCongGao.lean
import took 1.71s
cumulative profiling times:
attribute application 0.0141ms
elaboration 13.7ms
fix level params 0.0545ms
import 1.71s
initialization 33.8ms
instantiate metavars 0.081ms
interpretation 213ms
let-to-have transformation 0.0562ms
linting 1.92ms
module linting 0.00139ms
overlappingInstancesLinter 0.713ms
parsing 3.05ms
process pre-definitions 0.565ms
share common exprs 0.436ms
tactic execution 15ms
tacticAnalysis 6.48ms
type checking 2.82ms
typeclass inference 11.7ms
real 2.64
user 1.49
sys 1.18
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
Vilin97
requested changes
Sep 1, 2026
Vilin97
left a comment
Vilin97
left a comment
Owner
There was a problem hiding this comment.
Reviewed exact draft head 05e2268d8e26a07acfb8149422f04d8e0317a561.
The comparator check is green and the proof profile is reasonable for a 3,325-LOC development (334 maxHB; 55.19 s changed-module wall time), but this head cannot be accepted in its current shape:
- It adds
Challenge/WeiLiCongGao.leanand the matchingSolution/in one PR. Under the solution rules, a solution must not touch the challenge statement it claims to solve. The maintainer has also directed that this already-solved result be submitted as a project rather than an open challenge. - Exact-head Lean Action CI fails because the project emits repository-blocking warnings: misplaced module docstrings in
Ranges.lean,TrigSigns.lean,TanExpressions.lean, andEndgame.lean, plus the broadimport Mathlib.TacticinEndgame.lean. - The pooled project currently leaves the final theorem with the original geometric hypotheses only in
Solution/WeiLiCongGao.lean; its registered headline is the conditionalsix_distances_of_parametrization. A project-only revision should expose and register the final E2 theorem in the pooled project itself.
Please convert this to a ready-for-review pooled-project PR, remove the challenge/solution lifecycle changes, fix all warning-producing imports/docstrings, expose the final E2 theorem as a project result, and obtain green required CI. Keep the card explicit that this is the independently significant repaired E2 step; it does not completely solve Erdős problem 132.
Owner
|
Supplement to the current-head changes request: the DOI metadata and paper itself list the authors of 10.11650/tjm.18.2014.4030 as Xianglin Wei, Guogang Li, Yue Cong, and Feixing Gao. This PR records Zhengyu Li, Meiqin Cong, and Yan Gao after the first author. Please correct the source attribution in the registry/project card when converting this result to a pooled project. Authoritative DOI metadata: https://api.crossref.org/works/10.11650/tjm.18.2014.4030 |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #358 — the first commit is that challenge; this adds its solution. Marked draft until #358 lands; if it is simpler to take both at once, this PR alone brings the challenge entry already flipped to
status: solved.Solution/WeiLiCongGao.leanrestatesChallenge.WeiLiCongGao.e2_pattern_six_distancesunder the same name and proves it from the new project moduleLeanPool/Erdos132WeiE2(registered inprojects.yml, provenance: AI). It does not import the challenge module.Proof shape, five layers: any two unit segments among points of pairwise distance ≤ 1 intersect → the seven diameters pairwise cross, forcing the star-heptagon structure → exact angle parametrization on the diameter cycle with angle sum π → the seven undetermined diagonals collapse into three algebraic classes with forced strict inequalities, leaving three five-distance label assignments → each assignment dies by an explicit Bezout identity certifying its unit ideal (
linear_combination); the diameter-cycle geometry layer is new — Mathlib has no diameter-graph theory.Receipts, all local: build sorry-free;
#print axiomsexactly[propext, Classical.choice, Quot.sound]; comparator: "Verified: challenge 'diameter-heptagon-e2-six-distances' is proved by the solution" (macOS--insecure-no-sandbox);runLinter+lint-styleexit 0 on all three libraries.🤖 Generated with Claude Code