Add @[proof_condition] attribute for conditional formal proofs

.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',

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 "<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

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
@@ -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 exclude.contains "proofConditions" || 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

site/build.js

@@ -195,6 +195,7 @@ function processEntry(entry) {
     hasFormalProof,
     formalProofKind: entry.formalProofKind || null,
     formalProofLink: entry.formalProofLink || null,
+    proofConditions: entry.proofConditions || [],
   };
 }
 

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; }

site/src/js/theorem.js

@@ -489,6 +489,15 @@ function renderDetail(theorem, siblings, verso, contributors) {
       </div>
     </div>` : '';
 
+  // Proof conditions: unproven assumptions the formal proof depends on.
+  const proofConditions = theorem.proofConditions || [];
+  const proofConditionsSection = proofConditions.length ? `
+    <div class="theorem-detail__section">
+      <div class="detail-label">Proof conditions</div>
+      <div class="detail-value">The formal proof holds under
+        ${proofConditions.map(c => `<code>${FC.escapeHTML(c)}</code>`).join(', ')}.</div>
+    </div>` : '';
+
   const contributorsSection = contributors.length ? `
     <div class="theorem-detail__section">
       <div class="detail-label">File contributors</div>
@@ -507,6 +516,8 @@ function renderDetail(theorem, siblings, verso, contributors) {
     <header class="theorem-detail__header">
       <h1 class="theorem-detail__title">${FC.escapeHTML(theorem.displayTheorem)}</h1>
       <span class="badge ${catMeta.css}" style="font-size:.9rem;padding:.3rem .9rem">${FC.escapeHTML(catMeta.label)}</span>
+      ${proofConditions.length ? `<span class="badge cat-conditional" style="font-size:.9rem;padding:.3rem .9rem"
+        title="The formal proof depends on an unproven assumption">Conditional</span>` : ''}
     </header>
 
     ${moduleDocSection}
@@ -515,6 +526,8 @@ function renderDetail(theorem, siblings, verso, contributors) {
 
     ${codeSection}
 
+    ${proofConditionsSection}
+
     ${contributorsSection}
 
     <div class="theorem-detail__section">