From 41735efaa3e5509ceaaadb8ace94b4dd7f50546b Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Wed, 1 Jul 2026 11:59:03 -0400 Subject: [PATCH 1/5] Add @[proof_condition] attribute for conditional formal proofs Some solved problems have a formal proof that holds only under an unproven assumption such as GRH. The repository already flags these by naming convention (`conditional_artin_primitive_roots`, with a `(h : type_of% generalized_riemann_hypothesis)` hypothesis), but the condition is not machine-readable: `extract_names` and the site cannot distinguish a conditional proof from an unconditional one. Add a `@[proof_condition "..."]` attribute, repeatable with one condition per application, mirroring the existing `formal_proof` and `category` infrastructure. `extract_names` emits a `proofConditions` field, `build.js` carries it to the client, and the theorem page shows a "Conditional" badge and a "Proof conditions" line. Annotate the four `conditional_artin_primitive_roots` theorems with `proof_condition "GRH"` as the first use. --- .github/workflows/build-and-docs.yml | 1 + FormalConjectures/Util/Attributes/Basic.lean | 73 +++++++++++++++++++ .../ArtinPrimitiveRootsConjecture.lean | 8 +- scripts/extract_names.lean | 13 ++++ site/build.js | 1 + site/src/css/style.css | 1 + site/src/js/theorem.js | 13 ++++ 7 files changed, 106 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build-and-docs.yml b/.github/workflows/build-and-docs.yml index 75b5a7f425..d6619f1739 100644 --- a/.github/workflows/build-and-docs.yml +++ b/.github/workflows/build-and-docs.yml @@ -233,6 +233,7 @@ jobs: formalProofKind: c.formalProofKind || null, formalProofLink: c.formalProofLink || null, hasSorryFreeProof: false, + proofConditions: c.proofConditions || [], })); fs.writeFileSync( 'site/data/conjectures.json', diff --git a/FormalConjectures/Util/Attributes/Basic.lean b/FormalConjectures/Util/Attributes/Basic.lean index 80ff7a4afb..da6c48dd5b 100644 --- a/FormalConjectures/Util/Attributes/Basic.lean +++ b/FormalConjectures/Util/Attributes/Basic.lean @@ -83,6 +83,30 @@ theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := b sorry ``` +## The Proof Condition Attribute: + +### Overview +Records an unproven assumption that a formal proof depends on. This is the +structured counterpart to the `conditional_*` naming convention already used in +the repository (e.g. `conditional_artin_primitive_roots`): a proof can be +`sorry`-free and still establish the statement only under a hypothesis such as +GRH, so a reader and the site can see the condition rather than infer it from a +declaration name. + +Use it alongside `formal_proof` when the proof it points to is conditional. The +attribute is repeatable, one condition per application. + +### Values +- `@[proof_condition "GRH"]` : the proof holds under the Generalized Riemann Hypothesis. +- `@[proof_condition "Maynard–Tao"]` : the proof assumes the Maynard–Tao theorem. + +### Usage example +``` +@[category research solved, proof_condition "GRH"] +theorem conditional_result (h : type_of% generalized_riemann_hypothesis) : ... := by + sorry +``` + ## The Problem Subject Attribute Provides information about the subject of a mathematical problem, via a @@ -211,6 +235,28 @@ def addFormalProofEntry {m : Type → Type} [MonadEnv m] modifyEnv (formalProofExt.addEntry · { declName := declName, proofKind := kind, proofLink := link }) +/-- A tag recording an unproven assumption a formal proof depends on. -/ +structure ProofConditionTag where + /-- The name of the declaration with the given tag. -/ + declName : Name + /-- A human-readable description of the condition (e.g. "GRH"). -/ + condition : String + deriving Inhabited, BEq, Hashable, ToExpr + +/-- Defines the `proofConditionExt` extension for recording the unproven +assumptions a formal proof depends on. -/ +initialize proofConditionExt : + SimplePersistentEnvExtension ProofConditionTag (Std.HashSet ProofConditionTag) ← + registerSimplePersistentEnvExtension { + addImportedFn := fun as => as.foldl Std.HashSet.insertMany {} + addEntryFn := .insert + } + +def addProofConditionEntry {m : Type → Type} [MonadEnv m] + (declName : Name) (condition : String) : m Unit := + modifyEnv (proofConditionExt.addEntry · + { declName := declName, condition := condition }) + structure SubjectTag where /-- The name of the declaration with the given tag. -/ declName : Name @@ -317,6 +363,25 @@ initialize Lean.registerBuiltinAttribute { applicationTime := .afterTypeChecking } +syntax (name := ProofCondition_attr) "proof_condition" str : attr + +/-- Records an unproven assumption a formal proof depends on. + +Use alongside `formal_proof` when the proof it points to is conditional. The +attribute is repeatable, one condition per application. + +Usage: `@[proof_condition ""]`, e.g. `@[proof_condition "GRH"]`. -/ +initialize Lean.registerBuiltinAttribute { + name := `ProofCondition_attr + descr := "Annotation of an unproven assumption a formal proof depends on." + add := fun decl stx _attrKind => do + match stx with + | `(attr| proof_condition $cond) => + addProofConditionEntry decl cond.getString + | _ => throwUnsupportedSyntax + applicationTime := .afterTypeChecking +} + syntax subjectList := many(num) /-- Converts a syntax node to an array of `AMS` subjects. @@ -395,6 +460,14 @@ def getFormalProofTag (declName : Name) : m (Option FormalProofTag) := do let tags ← getFormalProofTags return tags.find? (·.declName == declName) +def getProofConditionTags : m (Array ProofConditionTag) := do + return proofConditionExt.getState (← MonadEnv.getEnv) |>.toArray + +/-- Get the conditions a given declaration's proof depends on. -/ +def getProofConditions (declName : Name) : m (Array String) := do + let tags ← getProofConditionTags + return (tags.filter (·.declName == declName)).map (·.condition) + end Helper /-- Verify that the list of problems contains the expected number of problems diff --git a/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean b/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean index cd69744dbe..8ead7e3986 100644 --- a/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean +++ b/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean @@ -97,7 +97,7 @@ theorem artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ /-- **Artin's Conjecture on Primitive Roots**, first half, conditional on GRH. -/ -@[category research solved, AMS 11] +@[category research solved, AMS 11, proof_condition "GRH"] theorem conditional_artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) (h : type_of% generalized_riemann_hypothesis) : ∃ x > 0, (S a).HasDensity x {p | p.Prime} := by @@ -122,7 +122,7 @@ theorem artin_primitive_roots.parts.ii /-- **Artin's Conjecture on Primitive Roots**, second half, conditional on GRH. -/ -@[category research solved, AMS 11] +@[category research solved, AMS 11, proof_condition "GRH"] theorem conditional_artin_primitive_roots.parts.ii (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2) (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0) @@ -161,7 +161,7 @@ theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_on /-- **Artin's Conjecture on Primitive Roots**, second half, power version, conditional on GRH -/ -@[category research solved, AMS 11] +@[category research solved, AMS 11, proof_condition "GRH"] theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4]) @@ -191,7 +191,7 @@ theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one /-- **Artin's Conjecture on Primitive Roots**, second half, power version, conditional on GRH. -/ -@[category research solved, AMS 11] +@[category research solved, AMS 11, proof_condition "GRH"] theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) diff --git a/scripts/extract_names.lean b/scripts/extract_names.lean index 7025313328..89c3d938a2 100644 --- a/scripts/extract_names.lean +++ b/scripts/extract_names.lean @@ -128,6 +128,7 @@ structure TheoremInfo where hasSorryFreeProof : Bool subsets : List String answerKinds : List String + proofConditions : List String fileFirstAdded : Option String fileLastModified : Option String @@ -150,6 +151,8 @@ def TheoremInfo.toFilteredJson (info : TheoremInfo) (exclude : Std.HashSet Strin ++ (if info.subsets.isEmpty then [] else [("subsets", toJson info.subsets)]) ++ (if exclude.contains "answerKinds" then [] else [("answerKinds", toJson info.answerKinds)]) + ++ (if info.proofConditions.isEmpty then [] else + [("proofConditions", toJson info.proofConditions)]) ++ (if exclude.contains "fileFirstAdded" then [] else [("fileFirstAdded", toJson info.fileFirstAdded)]) ++ (if exclude.contains "fileLastModified" then [] else @@ -228,6 +231,7 @@ unsafe def main (args : List String) : IO Unit := do let tags ← getTags let subjectTags ← getSubjectTags let formalProofTags ← getFormalProofTags + let proofConditionTags ← getProofConditionTags -- Create maps for quick lookup let mut categoryMap : Std.HashMap Name (List String) := {} @@ -241,6 +245,12 @@ unsafe def main (args : List String) : IO Unit := do for tag in formalProofTags do formalProofMap := formalProofMap.insert tag.declName tag + -- Create proof condition map (a declaration may carry several conditions) + let mut proofConditionMap : Std.HashMap Name (List String) := {} + for tag in proofConditionTags do + proofConditionMap := proofConditionMap.insert tag.declName + (tag.condition :: proofConditionMap.getD tag.declName []) + let mut subjectMap : Std.HashMap Name (List String) := {} for tag in subjectTags do let subjects := tag.subjects.map (fun (s : AMS) => s!"{s.toNat?.get!}") @@ -301,6 +311,8 @@ unsafe def main (args : List String) : IO Unit := do IO.eprintln s!"WARNING: Theorem {name} is categorised as `API` but has no sorry-free proof" | _, _ => pure () let subsets := (theoremToSubsets.getD name []).toArray.qsort (· < ·) |>.toList + let proofConditions := + (proofConditionMap.getD name []).toArray.qsort (· < ·) |>.toList -- Determine answerKinds from the elaborated type let answerKinds ← Meta.MetaM.run' (getAnswerKinds info.type) @@ -318,6 +330,7 @@ unsafe def main (args : List String) : IO Unit := do hasSorryFreeProof := hasSorryFreeProof, subsets := subsets answerKinds := answerKinds + proofConditions := proofConditions fileFirstAdded := fileFirstAdded fileLastModified := fileLastModified } :: allResults diff --git a/site/build.js b/site/build.js index 3005b10441..a8b37e8566 100644 --- a/site/build.js +++ b/site/build.js @@ -195,6 +195,7 @@ function processEntry(entry) { hasFormalProof, formalProofKind: entry.formalProofKind || null, formalProofLink: entry.formalProofLink || null, + proofConditions: entry.proofConditions || [], }; } diff --git a/site/src/css/style.css b/site/src/css/style.css index 7f79262eb5..8704253a94 100644 --- a/site/src/css/style.css +++ b/site/src/css/style.css @@ -430,6 +430,7 @@ a.cat-stat:hover { text-decoration: none; opacity: 0.8; } color: #064e3b; border: 1px solid #6ee7b7; } +.cat-conditional { background: #fff7ed; color: #9a3412; border: 1px solid #fed7aa; } .cat-textbook { background: var(--cat-grad-bg); color: #1e40af; border: 1px solid #bfdbfe; } .cat-test { background: var(--cat-other-bg); color: #374151; border: 1px solid #e5e7eb; } .cat-api { background: var(--cat-other-bg); color: #374151; border: 1px solid #e5e7eb; } diff --git a/site/src/js/theorem.js b/site/src/js/theorem.js index 1f54a950df..2d2473096f 100644 --- a/site/src/js/theorem.js +++ b/site/src/js/theorem.js @@ -489,6 +489,15 @@ function renderDetail(theorem, siblings, verso, contributors) { ` : ''; + // Proof conditions: unproven assumptions the formal proof depends on. + const proofConditions = theorem.proofConditions || []; + const proofConditionsSection = proofConditions.length ? ` +
+
Proof conditions
+
The formal proof holds under + ${proofConditions.map(c => `${FC.escapeHTML(c)}`).join(', ')}.
+
` : ''; + const contributorsSection = contributors.length ? `
File contributors
@@ -507,6 +516,8 @@ function renderDetail(theorem, siblings, verso, contributors) {

${FC.escapeHTML(theorem.displayTheorem)}

${FC.escapeHTML(catMeta.label)} + ${proofConditions.length ? `Conditional` : ''}
${moduleDocSection} @@ -515,6 +526,8 @@ function renderDetail(theorem, siblings, verso, contributors) { ${codeSection} + ${proofConditionsSection} + ${contributorsSection}
From b825546300213d0ddcabedbe7186eb8db54772c2 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Wed, 1 Jul 2026 13:54:41 -0400 Subject: [PATCH 2/5] Fix proof condition metadata extraction --- .../Wikipedia/ArtinPrimitiveRootsConjecture.lean | 8 ++++---- scripts/extract_names.lean | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean b/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean index 8ead7e3986..cd69744dbe 100644 --- a/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean +++ b/FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean @@ -97,7 +97,7 @@ theorem artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ /-- **Artin's Conjecture on Primitive Roots**, first half, conditional on GRH. -/ -@[category research solved, AMS 11, proof_condition "GRH"] +@[category research solved, AMS 11] theorem conditional_artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) (h : type_of% generalized_riemann_hypothesis) : ∃ x > 0, (S a).HasDensity x {p | p.Prime} := by @@ -122,7 +122,7 @@ theorem artin_primitive_roots.parts.ii /-- **Artin's Conjecture on Primitive Roots**, second half, conditional on GRH. -/ -@[category research solved, AMS 11, proof_condition "GRH"] +@[category research solved, AMS 11] theorem conditional_artin_primitive_roots.parts.ii (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2) (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0) @@ -161,7 +161,7 @@ theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_on /-- **Artin's Conjecture on Primitive Roots**, second half, power version, conditional on GRH -/ -@[category research solved, AMS 11, proof_condition "GRH"] +@[category research solved, AMS 11] theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4]) @@ -191,7 +191,7 @@ theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one /-- **Artin's Conjecture on Primitive Roots**, second half, power version, conditional on GRH. -/ -@[category research solved, AMS 11, proof_condition "GRH"] +@[category research solved, AMS 11] theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) diff --git a/scripts/extract_names.lean b/scripts/extract_names.lean index 89c3d938a2..a44ba397c9 100644 --- a/scripts/extract_names.lean +++ b/scripts/extract_names.lean @@ -113,8 +113,8 @@ def getFileLastModified (file : System.FilePath) : IO (Option String) := /-- Valid keys for the `--exclude` flag. -/ def validExcludeKeys : List String := ["docstring", "statement", "subjects", "formalProofKind", "formalProofLink", - "hasSorryFreeProof", "moduleDocstrings", "answerKinds", "fileFirstAdded", - "fileLastModified"] + "hasSorryFreeProof", "moduleDocstrings", "answerKinds", "proofConditions", + "fileFirstAdded", "fileLastModified"] structure TheoremInfo where «theorem» : String @@ -151,7 +151,7 @@ def TheoremInfo.toFilteredJson (info : TheoremInfo) (exclude : Std.HashSet Strin ++ (if info.subsets.isEmpty then [] else [("subsets", toJson info.subsets)]) ++ (if exclude.contains "answerKinds" then [] else [("answerKinds", toJson info.answerKinds)]) - ++ (if info.proofConditions.isEmpty then [] else + ++ (if exclude.contains "proofConditions" || info.proofConditions.isEmpty then [] else [("proofConditions", toJson info.proofConditions)]) ++ (if exclude.contains "fileFirstAdded" then [] else [("fileFirstAdded", toJson info.fileFirstAdded)]) From d0ec99cc2e98781e3c912f36b386bfd9a6d8613a Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Thu, 2 Jul 2026 10:05:09 -0400 Subject: [PATCH 3/5] Rework as conditional formal_proof ... assuming Per review: fold the separate @[proof_condition] attribute into formal_proof as an optional `conditional` modifier (Paul-Lez), and record the assumed hypotheses as named declarations stated in the same file with sorry proofs, referenced from an `assuming` clause (mo271). @[conditional formal_proof using lean4 at "" assuming grh] The hypothesis idents are resolved against the environment (unknown names error, hovers jump to the statement), `conditional` without `assuming` and vice versa are errors, and a sorry-free hypothesis triggers a warning that the proof may no longer be conditional. extract_names emits the fully-qualified declaration names under the existing proofConditions key. --- FormalConjectures/Util/Attributes/Basic.lean | 173 +++++++++---------- scripts/extract_names.lean | 11 +- site/src/js/theorem.js | 10 +- 3 files changed, 91 insertions(+), 103 deletions(-) diff --git a/FormalConjectures/Util/Attributes/Basic.lean b/FormalConjectures/Util/Attributes/Basic.lean index da6c48dd5b..13cd961d1c 100644 --- a/FormalConjectures/Util/Attributes/Basic.lean +++ b/FormalConjectures/Util/Attributes/Basic.lean @@ -58,6 +58,20 @@ This is independent of the category attribute and can be used with any category. - `@[formal_proof using other_system at "link"]` : formally proved in another system (Roqc, Isabelle, Lean 3, HOL, etc.) +### Conditional formal proofs +A formal proof that only establishes the statement under an unproven hypothesis +(such as GRH) is marked with the `conditional` modifier. Each hypothesis is stated +as a declaration in the same file (with a `sorry` proof) and named in the +`assuming` clause: +- `@[conditional formal_proof using lean4 at "link" assuming grh]` : formally proved + in Lean 4 elsewhere, assuming the statement of the declaration `grh`. + +This is the structured counterpart to the `conditional_*` naming convention already +used in the repository (e.g. `conditional_artin_primitive_roots`): a proof can be +`sorry`-free and still establish the statement only under an unproven hypothesis, +so a reader and the site can see exactly what is assumed rather than infer it from +a declaration name. + ### Usage examples The tag should be used as follows: ``` @@ -78,32 +92,18 @@ theorem an_open_problem : Transcendental ℝ (π + rexp 1) := by theorem a_solved_problem_with_formal_proof : ... := by sorry -@[category test] -theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := by +/-- The unproven hypothesis assumed by the conditional proof below (statement only). -/ +@[category research open] +theorem grh : ... := by sorry -``` - -## The Proof Condition Attribute: - -### Overview -Records an unproven assumption that a formal proof depends on. This is the -structured counterpart to the `conditional_*` naming convention already used in -the repository (e.g. `conditional_artin_primitive_roots`): a proof can be -`sorry`-free and still establish the statement only under a hypothesis such as -GRH, so a reader and the site can see the condition rather than infer it from a -declaration name. - -Use it alongside `formal_proof` when the proof it points to is conditional. The -attribute is repeatable, one condition per application. -### Values -- `@[proof_condition "GRH"]` : the proof holds under the Generalized Riemann Hypothesis. -- `@[proof_condition "Maynard–Tao"]` : the proof assumes the Maynard–Tao theorem. +@[category research solved, + conditional formal_proof using lean4 at "https://example.com/proof" assuming grh] +theorem a_conditionally_proved_problem : ... := by + sorry -### Usage example -``` -@[category research solved, proof_condition "GRH"] -theorem conditional_result (h : type_of% generalized_riemann_hypothesis) : ... := by +@[category test] +theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := by sorry ``` @@ -220,6 +220,9 @@ structure FormalProofTag where proofKind : FormalProofKind /-- A link to the formal proof. -/ proofLink : String + /-- Declarations (stated in the same file, with `sorry` proofs) for the unproven + hypotheses the proof assumes. Empty for an unconditional proof. -/ + conditions : List Name := [] deriving Inhabited, BEq, Hashable, ToExpr /-- Defines the `formalProofExt` extension for recording formal proof annotations. -/ @@ -231,31 +234,11 @@ initialize formalProofExt : } def addFormalProofEntry {m : Type → Type} [MonadEnv m] - (declName : Name) (kind : FormalProofKind) (link : String) : m Unit := + (declName : Name) (kind : FormalProofKind) (link : String) + (conditions : List Name := []) : m Unit := modifyEnv (formalProofExt.addEntry · - { declName := declName, proofKind := kind, proofLink := link }) - -/-- A tag recording an unproven assumption a formal proof depends on. -/ -structure ProofConditionTag where - /-- The name of the declaration with the given tag. -/ - declName : Name - /-- A human-readable description of the condition (e.g. "GRH"). -/ - condition : String - deriving Inhabited, BEq, Hashable, ToExpr - -/-- Defines the `proofConditionExt` extension for recording the unproven -assumptions a formal proof depends on. -/ -initialize proofConditionExt : - SimplePersistentEnvExtension ProofConditionTag (Std.HashSet ProofConditionTag) ← - registerSimplePersistentEnvExtension { - addImportedFn := fun as => as.foldl Std.HashSet.insertMany {} - addEntryFn := .insert - } - -def addProofConditionEntry {m : Type → Type} [MonadEnv m] - (declName : Name) (condition : String) : m Unit := - modifyEnv (proofConditionExt.addEntry · - { declName := declName, condition := condition }) + { declName := declName, proofKind := kind, proofLink := link, + conditions := conditions }) structure SubjectTag where /-- The name of the declaration with the given tag. -/ @@ -330,7 +313,9 @@ initialize Lean.registerBuiltinAttribute { applicationTime := .afterTypeChecking } -syntax (name := FormalProof_attr) "formal_proof" &"using" formalProofKind &"at" str : attr +syntax (name := FormalProof_attr) + (&"conditional")? "formal_proof" &"using" formalProofKind &"at" str + (&"assuming" ident,+)? : attr /-- Records the existence and location of a formal proof for a statement. @@ -339,46 +324,54 @@ This is independent of the `category` attribute and can be used with any categor Usage: `@[formal_proof using at ""]` where `` is one of: - `formal_conjectures` : formally proved in this repository. - `lean4` : formally proved in Lean 4 elsewhere (e.g. Mathlib). -- `other_system` : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.) -/ +- `other_system` : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.) + +A proof that only establishes the statement under unproven hypotheses is marked +`conditional` and names the hypotheses, each stated as a declaration in the same +file (with a `sorry` proof): +`@[conditional formal_proof using at "" assuming , ...]`. -/ initialize Lean.registerBuiltinAttribute { name := `FormalProof_attr descr := "Annotation of the existence and location of a formal proof." add := fun decl stx _attrKind => do - match stx with - | `(attr| formal_proof using $kind at $link) => do - let some n := formalProofKind.toName kind | throwUnsupportedSyntax - let pfKind ← Lean.Meta.MetaM.run' <| - unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) - Elab.addConstInfo kind n - -- Warn if this is attached to a `research open` problem. - let env ← getEnv - let catTags := categoryExt.getState env - if catTags.toArray.any fun tag => tag.declName == decl && - tag.category == .research .open then - logWarning - "A `formal_proof` annotation on a `research open` problem is suspicious. \ - If a formal proof exists, the problem should not be categorised as `open`." - addFormalProofEntry decl pfKind link.getString - | _ => throwUnsupportedSyntax - applicationTime := .afterTypeChecking -} - -syntax (name := ProofCondition_attr) "proof_condition" str : attr - -/-- Records an unproven assumption a formal proof depends on. - -Use alongside `formal_proof` when the proof it points to is conditional. The -attribute is repeatable, one condition per application. - -Usage: `@[proof_condition ""]`, e.g. `@[proof_condition "GRH"]`. -/ -initialize Lean.registerBuiltinAttribute { - name := `ProofCondition_attr - descr := "Annotation of an unproven assumption a formal proof depends on." - add := fun decl stx _attrKind => do - match stx with - | `(attr| proof_condition $cond) => - addProofConditionEntry decl cond.getString - | _ => throwUnsupportedSyntax + let (kind, link, conds) ← match stx with + | `(attr| formal_proof using $kind at $link) => + pure (kind, link, #[]) + | `(attr| conditional formal_proof using $kind at $link assuming $conds,*) => + pure (kind, link, conds.getElems) + | `(attr| conditional formal_proof using $_ at $_) => + throwError + "a `conditional` formal proof must name the hypotheses it assumes: \ + state each hypothesis as a declaration in this file (with a `sorry` proof) \ + and reference it as `conditional formal_proof using at \"\" \ + assuming `." + | `(attr| formal_proof using $_ at $_ assuming $_,*) => + throwError + "an `assuming` clause requires the `conditional` modifier: \ + `conditional formal_proof using at \"\" assuming `." + | _ => throwUnsupportedSyntax + let some n := formalProofKind.toName kind | throwUnsupportedSyntax + let pfKind ← Lean.Meta.MetaM.run' <| + unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) + Elab.addConstInfo kind n + let env ← getEnv + -- Resolve each assumed hypothesis to a declaration (so it is checked to exist + -- and hovering it jumps to the statement). + let conditions ← conds.toList.mapM fun (c : TSyntax `ident) => do + let condName ← resolveGlobalConstNoOverload c.raw + Elab.addConstInfo c.raw condName + if (env.find? condName).bind (·.value?) |>.any (!·.hasSorry) then + logWarning m!"The assumed hypothesis `{condName}` has a sorry-free proof, \ + so the formal proof may no longer need to be marked `conditional`." + return condName + -- Warn if this is attached to a `research open` problem. + let catTags := categoryExt.getState env + if catTags.toArray.any fun tag => tag.declName == decl && + tag.category == .research .open then + logWarning + "A `formal_proof` annotation on a `research open` problem is suspicious. \ + If a formal proof exists, the problem should not be categorised as `open`." + addFormalProofEntry decl pfKind link.getString conditions applicationTime := .afterTypeChecking } @@ -460,13 +453,11 @@ def getFormalProofTag (declName : Name) : m (Option FormalProofTag) := do let tags ← getFormalProofTags return tags.find? (·.declName == declName) -def getProofConditionTags : m (Array ProofConditionTag) := do - return proofConditionExt.getState (← MonadEnv.getEnv) |>.toArray - -/-- Get the conditions a given declaration's proof depends on. -/ -def getProofConditions (declName : Name) : m (Array String) := do - let tags ← getProofConditionTags - return (tags.filter (·.declName == declName)).map (·.condition) +/-- Get the unproven hypotheses a given declaration's formal proof assumes. +Empty when there is no formal proof or the proof is unconditional. -/ +def getProofConditions (declName : Name) : m (List Name) := do + let tag ← getFormalProofTag declName + return (tag.map (·.conditions)).getD [] end Helper diff --git a/scripts/extract_names.lean b/scripts/extract_names.lean index a44ba397c9..293c08cb0c 100644 --- a/scripts/extract_names.lean +++ b/scripts/extract_names.lean @@ -231,7 +231,6 @@ unsafe def main (args : List String) : IO Unit := do let tags ← getTags let subjectTags ← getSubjectTags let formalProofTags ← getFormalProofTags - let proofConditionTags ← getProofConditionTags -- Create maps for quick lookup let mut categoryMap : Std.HashMap Name (List String) := {} @@ -245,12 +244,6 @@ unsafe def main (args : List String) : IO Unit := do for tag in formalProofTags do formalProofMap := formalProofMap.insert tag.declName tag - -- Create proof condition map (a declaration may carry several conditions) - let mut proofConditionMap : Std.HashMap Name (List String) := {} - for tag in proofConditionTags do - proofConditionMap := proofConditionMap.insert tag.declName - (tag.condition :: proofConditionMap.getD tag.declName []) - let mut subjectMap : Std.HashMap Name (List String) := {} for tag in subjectTags do let subjects := tag.subjects.map (fun (s : AMS) => s!"{s.toNat?.get!}") @@ -311,8 +304,10 @@ unsafe def main (args : List String) : IO Unit := do IO.eprintln s!"WARNING: Theorem {name} is categorised as `API` but has no sorry-free proof" | _, _ => pure () let subsets := (theoremToSubsets.getD name []).toArray.qsort (· < ·) |>.toList + -- The unproven hypotheses a conditional formal proof assumes, + -- as declaration names. let proofConditions := - (proofConditionMap.getD name []).toArray.qsort (· < ·) |>.toList + ((formalProofMap.get? name).map (·.conditions.map Name.toString)).getD [] -- Determine answerKinds from the elaborated type let answerKinds ← Meta.MetaM.run' (getAnswerKinds info.type) diff --git a/site/src/js/theorem.js b/site/src/js/theorem.js index 2d2473096f..6fd7a56756 100644 --- a/site/src/js/theorem.js +++ b/site/src/js/theorem.js @@ -489,13 +489,15 @@ function renderDetail(theorem, siblings, verso, contributors) {
` : ''; - // Proof conditions: unproven assumptions the formal proof depends on. + // Unproven hypotheses a conditional formal proof assumes, as the names of + // declarations stated (with sorry proofs) in the same file. const proofConditions = theorem.proofConditions || []; const proofConditionsSection = proofConditions.length ? `
-
Proof conditions
-
The formal proof holds under - ${proofConditions.map(c => `${FC.escapeHTML(c)}`).join(', ')}.
+
Assumes
+
The formal proof assumes + ${proofConditions.map(c => `${FC.escapeHTML(c)}`).join(', ')}, + stated in this file.
` : ''; const contributorsSection = contributors.length ? ` From 52d4a493730b1b8b6a4bc8917bc429456ef34063 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Thu, 2 Jul 2026 13:10:04 -0400 Subject: [PATCH 4/5] Add conditional formal proof attribute tests --- FormalConjectures/Util/Attributes/Basic.lean | 94 +++++++++++-------- .../Util/Attributes/Basic.lean | 61 +++++++++++- 2 files changed, 112 insertions(+), 43 deletions(-) diff --git a/FormalConjectures/Util/Attributes/Basic.lean b/FormalConjectures/Util/Attributes/Basic.lean index 13cd961d1c..5d601c8d00 100644 --- a/FormalConjectures/Util/Attributes/Basic.lean +++ b/FormalConjectures/Util/Attributes/Basic.lean @@ -313,8 +313,11 @@ initialize Lean.registerBuiltinAttribute { applicationTime := .afterTypeChecking } -syntax (name := FormalProof_attr) - (&"conditional")? "formal_proof" &"using" formalProofKind &"at" str +syntax (name := FormalProof_attr) "formal_proof" &"using" formalProofKind &"at" str + (&"assuming" ident,+)? : attr + +syntax (name := conditional) + "conditional " "formal_proof" &"using" formalProofKind &"at" str (&"assuming" ident,+)? : attr /-- Records the existence and location of a formal proof for a statement. @@ -330,48 +333,57 @@ A proof that only establishes the statement under unproven hypotheses is marked `conditional` and names the hypotheses, each stated as a declaration in the same file (with a `sorry` proof): `@[conditional formal_proof using at "" assuming , ...]`. -/ +private def addFormalProofAttribute (decl : Name) (stx : Syntax) : AttrM Unit := do + let (kind, link, conds) ← match stx with + | `(attr| formal_proof using $kind at $link) => + pure (kind, link, #[]) + | `(attr| conditional formal_proof using $kind at $link assuming $conds,*) => + pure (kind, link, conds.getElems) + | `(attr| conditional formal_proof using $_ at $_) => + throwError + "a `conditional` formal proof must name the hypotheses it assumes: \ + state each hypothesis as a declaration in this file (with a `sorry` proof) \ + and reference it as `conditional formal_proof using at \"\" \ + assuming `." + | `(attr| formal_proof using $_ at $_ assuming $_,*) => + throwError + "an `assuming` clause requires the `conditional` modifier: \ + `conditional formal_proof using at \"\" assuming `." + | _ => throwUnsupportedSyntax + let some n := formalProofKind.toName kind | throwUnsupportedSyntax + let pfKind ← Lean.Meta.MetaM.run' <| + unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) + Elab.addConstInfo kind n + let env ← getEnv + -- Resolve each assumed hypothesis to a declaration (so it is checked to exist + -- and hovering it jumps to the statement). + let conditions ← conds.toList.mapM fun (c : TSyntax `ident) => do + let condName ← resolveGlobalConstNoOverload c.raw + Elab.addConstInfo c.raw condName + if (env.find? condName).bind (·.value?) |>.any (!·.hasSorry) then + logWarning m!"The assumed hypothesis `{condName}` has a sorry-free proof, \ + so the formal proof may no longer need to be marked `conditional`." + return condName + -- Warn if this is attached to a `research open` problem. + let catTags := categoryExt.getState env + if catTags.toArray.any fun tag => tag.declName == decl && + tag.category == .research .open then + logWarning + "A `formal_proof` annotation on a `research open` problem is suspicious. \ + If a formal proof exists, the problem should not be categorised as `open`." + addFormalProofEntry decl pfKind link.getString conditions + initialize Lean.registerBuiltinAttribute { name := `FormalProof_attr descr := "Annotation of the existence and location of a formal proof." - add := fun decl stx _attrKind => do - let (kind, link, conds) ← match stx with - | `(attr| formal_proof using $kind at $link) => - pure (kind, link, #[]) - | `(attr| conditional formal_proof using $kind at $link assuming $conds,*) => - pure (kind, link, conds.getElems) - | `(attr| conditional formal_proof using $_ at $_) => - throwError - "a `conditional` formal proof must name the hypotheses it assumes: \ - state each hypothesis as a declaration in this file (with a `sorry` proof) \ - and reference it as `conditional formal_proof using at \"\" \ - assuming `." - | `(attr| formal_proof using $_ at $_ assuming $_,*) => - throwError - "an `assuming` clause requires the `conditional` modifier: \ - `conditional formal_proof using at \"\" assuming `." - | _ => throwUnsupportedSyntax - let some n := formalProofKind.toName kind | throwUnsupportedSyntax - let pfKind ← Lean.Meta.MetaM.run' <| - unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) - Elab.addConstInfo kind n - let env ← getEnv - -- Resolve each assumed hypothesis to a declaration (so it is checked to exist - -- and hovering it jumps to the statement). - let conditions ← conds.toList.mapM fun (c : TSyntax `ident) => do - let condName ← resolveGlobalConstNoOverload c.raw - Elab.addConstInfo c.raw condName - if (env.find? condName).bind (·.value?) |>.any (!·.hasSorry) then - logWarning m!"The assumed hypothesis `{condName}` has a sorry-free proof, \ - so the formal proof may no longer need to be marked `conditional`." - return condName - -- Warn if this is attached to a `research open` problem. - let catTags := categoryExt.getState env - if catTags.toArray.any fun tag => tag.declName == decl && - tag.category == .research .open then - logWarning - "A `formal_proof` annotation on a `research open` problem is suspicious. \ - If a formal proof exists, the problem should not be categorised as `open`." - addFormalProofEntry decl pfKind link.getString conditions + add := fun decl stx _attrKind => addFormalProofAttribute decl stx + applicationTime := .afterTypeChecking +} + +initialize Lean.registerBuiltinAttribute { + name := `conditional + descr := "Annotation of a conditional formal proof and its assumed hypotheses." + add := fun decl stx _attrKind => addFormalProofAttribute decl stx applicationTime := .afterTypeChecking } diff --git a/FormalConjecturesTest/Util/Attributes/Basic.lean b/FormalConjecturesTest/Util/Attributes/Basic.lean index 6c5fc19f50..0d8ad17e53 100644 --- a/FormalConjecturesTest/Util/Attributes/Basic.lean +++ b/FormalConjecturesTest/Util/Attributes/Basic.lean @@ -45,8 +45,8 @@ theorem a_formally_solved_problem : 2 + 2 = 4 := by -- formal_proof on non-research categories #guard_msgs in -@[category graduate, AMS 11, formal_proof using lean4 at "https://github.com/example/proof"] -theorem a_graduate_problem_with_formal_proof : 1 + 1 = 2 := by +@[category textbook, AMS 11, formal_proof using lean4 at "https://github.com/example/proof"] +theorem a_textbook_problem_with_formal_proof : 1 + 1 = 2 := by rfl #guard_msgs in @@ -54,6 +54,63 @@ theorem a_graduate_problem_with_formal_proof : 1 + 1 = 2 := by theorem a_test_with_formal_proof : 3 + 3 = 6 := by rfl +#guard_msgs in +theorem conditional_formal_proof_hypothesis : 0 = 0 := by + sorry + +#guard_msgs in +theorem another_conditional_formal_proof_hypothesis : 1 = 1 := by + sorry + +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/conditional-proof" + assuming conditional_formal_proof_hypothesis] +theorem a_conditionally_formally_solved_problem : 4 + 4 = 8 := by + rfl + +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/two-hypotheses" + assuming conditional_formal_proof_hypothesis, another_conditional_formal_proof_hypothesis] +theorem a_conditionally_formally_solved_problem_with_two_hypotheses : 5 + 5 = 10 := by + rfl + +#eval do + let conditions ← ProblemAttributes.getProofConditions ``a_conditionally_formally_solved_problem + unless conditions = [``conditional_formal_proof_hypothesis] do + throwError "unexpected proof conditions for a_conditionally_formally_solved_problem" + +#eval do + let conditions ← ProblemAttributes.getProofConditions + ``a_conditionally_formally_solved_problem_with_two_hypotheses + unless conditions = [``conditional_formal_proof_hypothesis, + ``another_conditional_formal_proof_hypothesis] do + throwError + "unexpected proof conditions for a_conditionally_formally_solved_problem_with_two_hypotheses" + +/-- +error: a `conditional` formal proof must name the hypotheses it assumes: state each hypothesis as +a declaration in this file (with a `sorry` proof) and reference it as +`conditional formal_proof using at "" assuming `. +-/ +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/missing-hypothesis"] +theorem conditional_formal_proof_without_assuming : 6 + 6 = 12 := by + rfl + +/-- +error: an `assuming` clause requires the `conditional` modifier: +`conditional formal_proof using at "" assuming `. +-/ +#guard_msgs in +@[category research solved, + formal_proof using lean4 at "https://github.com/example/not-conditional" + assuming conditional_formal_proof_hypothesis] +theorem assuming_without_conditional_formal_proof : 7 + 7 = 14 := by + rfl + -- The `#AMS` command /-- From 5c61432f8d7f8a38c72a68140020daa70eed5cfd Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Fri, 3 Jul 2026 14:01:50 -0400 Subject: [PATCH 5/5] ci: retrigger after runner disk exhaustion (No space left on device, run 28608145267)