From ff18bcf5bc89b6618c6dd49c3304aabd827378ec Mon Sep 17 00:00:00 2001 From: "CYC.." Date: Thu, 22 Oct 2026 10:45:52 +0800 Subject: [PATCH 1/3] Record the current status of #109 on the openai/math card List the previous selected result (#1094), the selected one (#4359), the highest merged candidate (#4416) and the highest open claim (#4470). Co-Authored-By: Claude Sonnet 5.5 --- _includes/math/ai/OpenAIMath.html | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/_includes/math/ai/OpenAIMath.html b/_includes/math/ai/OpenAIMath.html index 1935b8a3..7bb337c5 100644 --- a/_includes/math/ai/OpenAIMath.html +++ b/_includes/math/ai/OpenAIMath.html @@ -27,7 +27,9 @@

#109

From 3f4662e3a3d38a064879d5e6962ee48dfdc0e0e0 Mon Sep 17 00:00:00 2001 From: "CYC.." Date: Thu, 22 Oct 2026 10:51:40 +0800 Subject: [PATCH 2/3] Nest the #109 status list and link each PR to GitHub Group the previous selected, selected, merged and open entries under one Status item, with a GitHub icon link after each PR number. Co-Authored-By: Claude Sonnet 5.5 --- _includes/math/ai/OpenAIMath.html | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/_includes/math/ai/OpenAIMath.html b/_includes/math/ai/OpenAIMath.html index 7bb337c5..ea1f6911 100644 --- a/_includes/math/ai/OpenAIMath.html +++ b/_includes/math/ai/OpenAIMath.html @@ -27,9 +27,13 @@

#109

  • CrocSwap/integer-mult-bounds GitHub: a community effort to optimize the construction and push $\kappa$ higher. It is conditional on the #109 framework and is not an official OpenAI release.
    • -
  • Previous selected: #1094, $\kappa\approx 0.00167$ (about $2^{-9.2}$).
    • -
  • Selected: #4359, $\kappa=0.0023$ (above $2^{-9}$), maintainer-reviewed but not a complete Lean multiplication theorem.
    • -
  • Merged but not selected: #4416, $\kappa=0.00268647$. Highest open claim: #4470, $\kappa=0.00302015$ (author-checked).
    • +
  • Status: +
      +
    • Previous selected: #1094 GitHub, $\kappa\approx 0.00167$ (about $2^{-9.2}$).
      • +
    • Selected: #4359 GitHub, $\kappa=0.0023$ (above $2^{-9}$), maintainer-reviewed but not a complete Lean multiplication theorem.
      • +
    • Merged but not selected: #4416 GitHub, $\kappa=0.00268647$. Highest open claim: #4470 GitHub, $\kappa=0.00302015$ (author-checked).
      • +
    +
  • Notes: CrocSwap integer-mult-bounds
From 26028533a21f5e9091bb0738d32425b0491a94dc Mon Sep 17 00:00:00 2001 From: "CYC.." Date: Thu, 22 Oct 2026 10:52:33 +0800 Subject: [PATCH 3/3] Put the highest open claim on its own line in the status list Co-Authored-By: Claude Sonnet 5.5 --- _includes/math/ai/OpenAIMath.html | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/_includes/math/ai/OpenAIMath.html b/_includes/math/ai/OpenAIMath.html index ea1f6911..fabaa3f7 100644 --- a/_includes/math/ai/OpenAIMath.html +++ b/_includes/math/ai/OpenAIMath.html @@ -31,7 +31,8 @@

#109

  • Previous selected: #1094 GitHub, $\kappa\approx 0.00167$ (about $2^{-9.2}$).
  • Selected: #4359 GitHub, $\kappa=0.0023$ (above $2^{-9}$), maintainer-reviewed but not a complete Lean multiplication theorem.
    • -
  • Merged but not selected: #4416 GitHub, $\kappa=0.00268647$. Highest open claim: #4470 GitHub, $\kappa=0.00302015$ (author-checked).
    • +
  • Merged but not selected: #4416 GitHub, $\kappa=0.00268647$.
    • +
  • Highest open claim: #4470 GitHub, $\kappa=0.00302015$ (author-checked).
  • Notes: CrocSwap integer-mult-bounds