Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

The original analytic aggregate bound for admissible selected minors

Proved
OAI.PiExponent.LiteralAnalytic.analyticAggregate

by Yuxuan Xu · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

For every real ν>2\nu>2ν>2 and fixed admissible datum ddd, there is an error ed(H)→0e_d(H)\to0ed​(H)→0 as H→+∞H\to+\inftyH→+∞. Eventually, every selected minor DDD with nonzero determinant satisfies

log⁡∥det⁡D∥Md(H)H≤ad+ed(H)+max⁡{−γd(H),−ν[Ad(1−ηd)−bd(H)]}.\frac{\log\|\det D\|}{M_d(H)H}\le a_d+e_d(H)+\max\{-\gamma_d(H),-\nu[A_d(1-\eta_d)-b_d(H)]\}.Md​(H)Hlog∥detD∥​≤ad​+ed​(H)+max{−γd​(H),−ν[Ad​(1−ηd​)−bd​(H)]}.

Here Md(H)M_d(H)Md​(H) is the row count, ada_dad​ the analytic error parameter, γd(H)\gamma_d(H)γd​(H) the collision rate, AdA_dAd​ and ηd\eta_dηd​ the fixed-data parameters, and bd(H)b_d(H)bd​(H) the normalized weighted row mean. The bound is uniform over the original column selections and is precisely the source analytic aggregate statement.

Preamble
import Definitions.Def_OAI_PiExponent_ApproximationDefinitions
import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_DeterminantContradiction_CoreData

open OAI.PiExponent OAI.PiExponent.DeterminantContradiction

Formal statement
theorem OAI.PiExponent.LiteralAnalytic.analyticAggregate : AnalyticAggregateStatement := by
  sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/AnalyticAggregate.lean#L96-L101

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me