Skip to content

catalog: record Lean formalization for JSP-000936 #1639

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Drag0ndddd1118 wants to merge 1 commit into from
Closed

catalog: record Lean formalization for JSP-000936 #1639

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion problems/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down
3 changes: 2 additions & 1 deletion problems/catalog-0901-1000.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)<br>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) |
Expand Down