Waring's problem for fourth powers
Is every sufficiently large number a sum of sixteen fourth powers?
▸Motivation
Waring 1770, Hilbert 1909 for the general existence. Davenport proved the sixteen-fourth-powers statement in 1939 — but ineffectively, meaning the proof gives no computable threshold.
That gap is the problem: it is known that only finitely many exceptions exist, and nobody can list them. Thirteen numbers up to 13792 are known to need seventeen.
Waring 1770; Davenport 1939 (ineffective).
▸Lean API
import Mathlib.NumberTheory.Divisors
namespace Conjectura.NT026
/-- Is every sufficiently large natural a sum of sixteen fourth powers? Davenport
proved it for all large enough n in 1939 without an effective bound; making the
threshold explicit, and reaching it by computation, is still not done. -/
def goal : Prop :=
∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ a : Fin 16 → ℕ, ∑ i, (a i) ^ 4 = n
end Conjectura.NT026▸Definition
This statement is written entirely in arithmetic and standard number systems — there is no specialised vocabulary to define.
▸Related work0
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem NT026 — Waring's problem for fourth powers
Is every sufficiently large number a sum of sixteen fourth powers?
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ a : Fin 16 → ℕ, ∑ i, (a i) ^ 4 = n := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.NT026.Statement
namespace Submission
theorem solution : Conjectura.NT026.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
(none)
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Submissions are not open yet
Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.
The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.