Add a conditional modifier and assuming clause to formal_proof

.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

@@ -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,6 +92,16 @@ theorem an_open_problem : Transcendental ℝ (π + rexp 1) := by
 theorem a_solved_problem_with_formal_proof : ... := by
   sorry
 
+/-- The unproven hypothesis assumed by the conditional proof below (statement only). -/
+@[category research open]
+theorem grh : ... := by
+  sorry
+
+@[category research solved,
+  conditional formal_proof using lean4 at "https://example.com/proof" assuming grh]
+theorem a_conditionally_proved_problem : ... := by
+  sorry
+
 @[category test]
 theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := by
   sorry
@@ -196,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. -/
@@ -207,9 +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 })
+    { declName := declName, proofKind := kind, proofLink := link,
+      conditions := conditions })
 
 structure SubjectTag where
   /-- The name of the declaration with the given tag. -/
@@ -284,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.
 
@@ -293,27 +324,54 @@ This is independent of the `category` attribute and can be used with any categor
 Usage: `@[formal_proof using <kind> at "<link>"]` where `<kind>` 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 <kind> at "<link>" assuming <decl>, ...]`. -/
 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
+    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 <kind> at \"<link>\" \
+           assuming <decl>`."
+      | `(attr| formal_proof using $_ at $_ assuming $_,*) =>
+        throwError
+          "an `assuming` clause requires the `conditional` modifier: \
+           `conditional formal_proof using <kind> at \"<link>\" assuming <decl>`."
+      | _ => 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
 }
 
@@ -395,6 +453,12 @@ def getFormalProofTag (declName : Name) : m (Option FormalProofTag) := do
   let tags ← getFormalProofTags
   return tags.find? (·.declName == declName)
 
+/-- 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
 
 /-- 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
@@ -301,6 +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 :=
+                ((formalProofMap.get? name).map (·.conditions.map Name.toString)).getD []
               -- Determine answerKinds from the elaborated type
               let answerKinds ← Meta.MetaM.run'
                 (getAnswerKinds info.type)
@@ -318,6 +325,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,17 @@ function renderDetail(theorem, siblings, verso, contributors) {
       </div>
     </div>` : '';
 
+  // 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 ? `
+    <div class="theorem-detail__section">
+      <div class="detail-label">Assumes</div>
+      <div class="detail-value">The formal proof assumes
+        ${proofConditions.map(c => `<code>${FC.escapeHTML(c)}</code>`).join(', ')},
+        stated in this file.</div>
+    </div>` : '';
+
   const contributorsSection = contributors.length ? `
     <div class="theorem-detail__section">
       <div class="detail-label">File contributors</div>
@@ -507,6 +518,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 +528,8 @@ function renderDetail(theorem, siblings, verso, contributors) {
 
     ${codeSection}
 
+    ${proofConditionsSection}
+
     ${contributorsSection}
 
     <div class="theorem-detail__section">