From 92cf87ab4f41261f62b5cc9c8d74df7cc108eb2f Mon Sep 17 00:00:00 2001 From: Qin Zhao Date: Sat, 19 Sep 2026 11:25:18 +0800 Subject: [PATCH] catalog: record Lean formalization for JSP-000936 --- problems/README.md | 2 +- problems/catalog-0901-1000.md | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/problems/README.md b/problems/README.md index effd358dd2..ff3a7ace41 100644 --- a/problems/README.md +++ b/problems/README.md @@ -1060,7 +1060,7 @@ The **No.** column runs consecutively from **JSP-000001** to **JSP-001022** in d | JSP-000933 | [Are the Boolean algebras of integer sets modulo zero natural density and modulo zero logarithmic density isomorphic?](catalog-0901-1000.md#JSP-000933) | Solved | No | No | Unavailable | | JSP-000934 | [Can a square and a disk of equal area be partitioned into finitely many pieces and reassembled into each other using the prescribed rigid motions?](catalog-0901-1000.md#JSP-000934) | Solved | No | No | Unavailable | | JSP-000935 | [Can Euclidean space be partitioned into countably many sets each having all pairwise distances distinct?](catalog-0901-1000.md#JSP-000935) | Solved | No | No | Unavailable | -| JSP-000936 | [Which Lagrange interpolation nodes minimize the maximum amplification of input errors?](catalog-0901-1000.md#JSP-000936) | Solved | No | No | Unavailable | +| JSP-000936 | [Which Lagrange interpolation nodes minimize the maximum amplification of input errors?](catalog-0901-1000.md#JSP-000936) | Solved | Yes | No | Unavailable | | JSP-000937 | [Which interpolation nodes maximize the smallest peak error-amplification factor among intervals between consecutive nodes?](catalog-0901-1000.md#JSP-000937) | Solved | No | No | Unavailable | | JSP-000938 | [What is the minimum sum of squared integrals of the Lagrange basis functions?](catalog-0901-1000.md#JSP-000938) | Open | No | No | Unavailable | | JSP-000939 | [For interpolation built from successive initial segments of an infinite node sequence, what lower bound must the amplification factor satisfy at a fixed point?](catalog-0901-1000.md#JSP-000939) | Open | No | No | Unavailable | diff --git a/problems/catalog-0901-1000.md b/problems/catalog-0901-1000.md index 3979aeb501..0e65b0ac2e 100644 --- a/problems/catalog-0901-1000.md +++ b/problems/catalog-0901-1000.md @@ -625,7 +625,8 @@ | Mathematical area | Analysis / Polynomials | | Problem description | Which Lagrange interpolation nodes minimize the maximum amplification of input errors? | | Current status | Solved | -| Lean proof | No | +| Lean proof | Yes — [Lean source](https://github.com/Drag0ndddd1118/jsp-000936-formalization/blob/63a776c/JSP_000936.lean)
Formalization contributors: OpenAI Codex, GPT-5.6 Sol. | +| Attribution basis | Community repository [ErdosProblems/lean-erdospb](https://github.com/ErdosProblems/lean-erdospb) ([Erdos1129.lean](https://github.com/ErdosProblems/lean-erdospb/blob/main/ErdosProblems/Erdos1129.lean)) formalizes Erdős Problem #1129 (Bernstein–Erdős optimal interpolation nodes; de Boor & Pinkus 1978 minimal Lebesgue constant and free-node non-uniqueness). Standalone verification repository: [Drag0ndddd1118/jsp-000936-formalization](https://github.com/Drag0ndddd1118/jsp-000936-formalization) (commit 63a776c). Disclosed prior community tracking and PRs: #121, #123, #129, #144, #764, #1404. | | Eligible to claim | No | | Historical bounty | | | Elapsed years | About 79 years (since 1947) |