Number theory

Gauss Circle Problem - error is Big O

It is conjectured that the correct bound is

|E(r)| = O\left(r^{1/2 + o(1)}\right)

[Ha59] Hardy, G. H. (1959). _Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work_(3rd ed.). New York: Chelsea Publishing Company. p. 67 See also https://arxiv.org/abs/2305.03549

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.Wikipedia.GaussCircleProblem
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "GaussCircleProblem.error_isBigO" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∃ o, ∃ (_ : Filter.Tendsto o Filter.atTop (nhds 0)), GaussCircleProblem.E =O[Filter.atTop] fun r => r ^ (1 / 2 + o r)

Original conjecture source: FormalConjectures/Wikipedia/GaussCircleProblem.lean

Source type SHA-256: sha256:1f76ab56a02baee83c2a82c5e205a500d35921f2db22f2c05378eacef44bb4ea
Task id: fc-v2-gausscircleproblem-error-isbigo-92b4c68496047c36f1807365-formalized
Task commitment: sha256:48ea9126565e7f7102be7004df0c3d719dfe1832fe847977e1f8412df3bdd29d

References

Wikipedia

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Gauss Circle Problem - error is Big O

It is conjectured that the correct bound is

|E(r)| = O\left(r^{1/2 + o(1)}\right)

[Ha59] Hardy, G. H. (1959). _Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work_(3rd ed.). New York: Chelsea Publishing Company. p. 67 See also https://arxiv.org/abs/2305.03549