From aa9723afa7384b093247b16ac18e33cc2c47fb4a Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 11 May 2026 17:21:24 +0200 Subject: [PATCH 1/3] hardy-ramanujan formula --- .../Combinatorics/PartitionAsymptotics.lean | 19 +++++++++++++++++++ manifests/problems.toml | 9 +++++++++ 2 files changed, 28 insertions(+) create mode 100644 LeanEval/Combinatorics/PartitionAsymptotics.lean diff --git a/LeanEval/Combinatorics/PartitionAsymptotics.lean b/LeanEval/Combinatorics/PartitionAsymptotics.lean new file mode 100644 index 0000000..f7bb0da --- /dev/null +++ b/LeanEval/Combinatorics/PartitionAsymptotics.lean @@ -0,0 +1,19 @@ +import Mathlib.Analysis.Asymptotics.Defs +import Mathlib.Combinatorics.Enumerative.Partition.Basic +import Mathlib.Analysis.Complex.Exponential +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic + +/-! # Asymptotic expression for the number of integer partitions + +Hardy and Ramanujan's asymptotic expression for the number of integer partitions. + +G. H. Hardy, S. Ramanujan. *Asymptotic formulae in combinatory analysis*, 1918. +-/ + +open Asymptotics Filter Fintype + +/-- Hardy and Ramanujan's asymptotic formula. -/ +@[eval_problem] +theorem isEquivalent_card_partition : + (fun (n : ℕ) => (card n.Partition : ℝ)) ~[atTop] + (fun n => Real.exp (Real.pi * Real.sqrt (2 * n / 3)) / (4 * n * Real.sqrt 3)) := sorry diff --git a/manifests/problems.toml b/manifests/problems.toml index d0d66c4..5ab255a 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -645,3 +645,12 @@ module = "LeanEval.NumberTheory.NeukirchUchida" holes = ["neukirch_uchida"] submitter = "Junyan Xu" source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1." + +[[problem]] +id = "asymptotic_partition" +title = "Hardy-Ramanujan asymptotic formula for the number of integer partitions" +test = false +module = "LeanEval.Combinatorics.PartitionAsymptotics" +holes = ["isEquivalent_card_partition"] +submitter = "Thomas K Waring" +source = "G. H. Hardy, S. Ramanujan. *Asymptotic formulae in combinatory analysis*, 1918." From 074bec21600f41fa27702cf89d30e931dea2825a Mon Sep 17 00:00:00 2001 From: thomaskwaring <51426330+thomaskwaring@users.noreply.github.com> Date: Mon, 11 May 2026 17:32:06 +0200 Subject: [PATCH 2/3] add informal solution --- manifests/problems.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/manifests/problems.toml b/manifests/problems.toml index 420aaff..1a82bc7 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -654,6 +654,7 @@ module = "LeanEval.Combinatorics.PartitionAsymptotics" holes = ["isEquivalent_card_partition"] submitter = "Thomas K Waring" source = "G. H. Hardy, S. Ramanujan. *Asymptotic formulae in combinatory analysis*, 1918." +informal_solution = "Evaluate the growth-rate of coefficients in the generating function by the so-called circle method." [[problem]] id = "balanceable_bounded_partitions" From 4ffd504ecce282a85c40274956376c6543e3a56e Mon Sep 17 00:00:00 2001 From: twwar Date: Tue, 12 May 2026 08:52:14 +0200 Subject: [PATCH 3/3] add import --- LeanEval/Combinatorics/PartitionAsymptotics.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanEval/Combinatorics/PartitionAsymptotics.lean b/LeanEval/Combinatorics/PartitionAsymptotics.lean index f7bb0da..858e7e9 100644 --- a/LeanEval/Combinatorics/PartitionAsymptotics.lean +++ b/LeanEval/Combinatorics/PartitionAsymptotics.lean @@ -1,3 +1,4 @@ +import EvalTools.Markers import Mathlib.Analysis.Asymptotics.Defs import Mathlib.Combinatorics.Enumerative.Partition.Basic import Mathlib.Analysis.Complex.Exponential