The first lake build this repository ever ran: 28 errors to 2 - #2761
Merged
Conversation
The first `lake build` this repository has ever run (#2759 added the job; this is what it said) failed with 28 errors, all in Trinity/NeutrinoMasses.lean. Nineteen distinct lines, three classes: 9 failed to compile definition, consider marking it as 'noncomputable' 8 unsolved goals 1 Type mismatch The nine are mechanical: `def Lambda_600 : ℝ := M_Planck / (h_H4 * phi)` and its neighbours divide over the reals, which Lean cannot compile without the marker. Marked. The other nine are NOT mechanical and are not touched here: `lemma h_H4_pos : 0 < h_H4 := by norm_num` and seven like it leave unsolved goals, and line 115 is a type mismatch. They may be a cascade from the first class -- the next dispatch answers that -- or they may be broken proofs. Either way that is a finding, not a formatting slip, and it belongs to #2747. This is what taking the measurement bought: 250 theorems that nothing had ever compiled, and the first build says the tree does not build. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Eight lemmas read `by norm_num` and left unsolved goals: norm_num does not unfold a `def`, so it never saw that h_H4 is 30 or that m_muon is 0.105658. The values were never in question; the tactic could not reach them. Lines 115-116 are left alone -- a type mismatch and a failed `apply`, which are real proof work and not a tactic that could not see a constant. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`apply div_lt_div_of_pos_right` was followed by (positivity, inequality). That
lemma takes them the other way round, so the first bullet was a type mismatch
and the `apply` beneath it could not unify -- the last two errors in the file.
Written through `div_eq_mul_inv` instead. `inv_pos`,
`mul_lt_mul_of_pos_right` and `div_eq_mul_inv` are stable names, so the proof
does not depend on which argument order the division lemma has in whichever
mathlib revision the toolchain pins.
lake build errors: 28 -> 16 -> 2 -> ?
Refs #2747
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
With NeutrinoMasses.lean clean, `lake build` moved to the next file and said the same thing: H4Lagrangian.lean:57, :60, :68, :83 divide or call Real.pi over the reals and cannot compile without the marker. Marked. The two theorems in that file are NOT touched. They already `unfold` their definitions and still leave unsolved goals, because the goals contain Real.pi and exp 1 and `norm_num` does not evaluate those -- proving `0.1 <= L01` needs numeric bounds on pi and e. That is mathematical content, not a tactic that could not see a constant, and it belongs in #2747 with the list rather than in a blind edit. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…r Koide Both theorems are true and both tactics could not reach a number. L01: norm_num does not evaluate Real.pi or Real.exp 1. L01 is 0.1695 against bounds of 0.1 and 1, so the claim has room to spare; what was missing is 0.8 < e/pi < 0.9, from the nine-digit bounds mathlib states. Koide: the expression contains sqrt 239 and sqrt 549. No tight bound is needed -- dividing by 2/3 the goal is 0 < K < 4/3, and K = 789/t^2 needs only t^2 > 591.75, which the crudest root bounds give. Those follow from (sqrt x)^2 = x and non-negativity, so no digit-level lemma is involved. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
lt_div_iff and div_lt_iff moved to the GroupWithZero order files and were renamed lt_div_iff₀ / div_lt_iff₀. The toolchain pins v4.31.0, where the unsuffixed names do not resolve -- three unknown identifiers in the previous attempt. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Real.pi_gt_3141592 does not exist in this revision. Real.pi_gt_314 and Real.pi_lt_315 are the long-standing pair and both margins hold with them: 0.8*3.15 = 2.52 < e and 0.9*3.14 = 2.826 > e, so two decimal places are enough. The Koide attempt is reverted. It reached unknown identifiers and a rewrite that found no occurrence -- the let bindings in Koide_H4 do not reduce the way the tactic assumed. The statement is true (0.2562 against a bound of 1) and the shape of the fix is written where the proof would go, but half a proof in the tree is worse than one named failure. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Real.pi_gt_3141592, Real.pi_lt_31415927, Real.pi_gt_314 and Real.pi_lt_315 are all unknown in this revision, while Real.pi_pos and Real.exp_one_gt_d9 resolve -- the bounds most likely sit behind an import this file does not have. Each guess costs a CI round, and someone with the mathlib API in front of them closes it in a minute. Both theorems are left with their original tactic and a comment stating: that the claim is TRUE and by how much (L01 = 0.1695 against 0.1 and 1; Koide 0.2562 against 1), what the proof needs, and what was already tried. That is worth more to the next reader than half a proof. Kept from the attempts: lt_div_iff₀ / div_lt_iff₀ DO resolve here, so the unsuffixed spellings are gone in this revision. Recorded in the comment. Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Refs #2747 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-28 19:21:38 UTC
Summary
Seal Status
|
Up to date for the ruleset; a rebase would need a force-push.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-28 19:25:56 UTC
Summary
Seal Status
|
gHashTag
added a commit
that referenced
this pull request
Aug 28, 2026
Up to date for the ruleset after #2761.
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
1 participant
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.
Refs #2747
lean-proofs.ymllanded in #2759 and was dispatched againstmaster— the firstlake buildthis repository has ever run. It failed, and every failure was real.NeutrinoMasses.leandefs over ℝ markednoncomputableunfold—norm_numdoes not unfold adef, so it never saw thath_H4is 30NeutrinoMasses.leanclean; the build moved on toH4Lagrangian.leannoncomputable, andseesaw_ordering's bullets were in the wrong order for its lemmaThree classes, none of them cosmetic: definitions over the reals that cannot compile without the marker, tactics that could not unfold a
defto reach a constant, and one proof whose bullets did not match its lemma's argument order.The two that remain are not fixed here, on purpose
Both statements are true, with margin:
L01_lagrangian_order_of_magnitudeKoide_H4_testL01needs a bound one/π; two decimal places suffice. Four names were tried, one CI round each —Real.pi_gt_3141592,Real.pi_lt_31415927,Real.pi_gt_314,Real.pi_lt_315— all unknown here, whileReal.pi_posandReal.exp_one_gt_d9resolve. The bounds most likely sit behind an import this file lacks.Koideneeds only0 < K < 4/3. An attempt reached a rewrite that found no occurrence — theletbindings inKoide_H4do not reduce the way the tactic assumed.Guessing lemma names down a four-minute feedback loop is the wrong instrument. Both attempts are reverted: half a proof in the tree is worse than one named failure. Each theorem now carries a comment saying the claim is true, by how much, what the proof needs, and what was already tried.
Kept from the attempts
lt_div_iffanddiv_lt_iffdo not resolve in this revision;lt_div_iff₀anddiv_lt_iff₀do. Recorded in the file, because the next person will hit it.🤖 Generated with Claude Code