Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

OAI.RuledApproximation.fullMain

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that FullMain holds, which is the conjunction of seven defined statements about covering ruled surfaces in R³ by finitely many infinite cylinders with small total cross-sectional area. A cylinder has a unit axis direction and a base set in the orthogonal complement plane of that axis; it consists of all points b + t·axis with b in the base and t real, and its area is the Lebesgue measure of the base. A finite cover has the cylinders of a prescribed shape (parallelogram, triangle, or open bounded measurable base), with the set contained in their union and the areas summing to at most a given bound. For a field v on the plane, ruled(D,v,L) is the set of points (p₁ + r v₁(p), p₂ + r v₂(p), r) with p in D and |r| ≤ L, and physicalRuled(h,D,v,L) is the set of points (s, p₁ + s v₁(p), h(p₂ + s v₂(p))) with |s| ≤ L. The weights are 1/√(1+‖v‖²) and 1/√(1+w₁²+h²w₂²). HyperbolicAt(L,v,p) means the derivative of v at p has eigenvalues λ and −λ with 0 < Lλ < 1. SmoothNear(n,D,v) means v is C^n on an open neighborhood of D. (1) For compact D, v C¹ near D, L > 0 and hyperbolic at every point of D, for every ε > 0 ruled(D,v,L) has a finite parallelogram cover of total area at most ∫_D 1/√(1+‖v‖²) + ε. (2) With h, L > 0 and the same hypotheses, for every ε > 0 and every isometry F of R³, F applied to physicalRuled(h,D,v,L) has a finite parallelogram cover of area at most h∫_D physicalWeight(h,v) + ε. (3) Logarithmic statement: for X, k > 0, compact D with null boundary, v C² on an open rectangle containing D, and at every point of D zero trace, negative determinant and kX√(−det) < 1 for the derivative of v, physicalRuled(1,D,kv,X) has a finite cover by open bounded measurable-base cylinders of area at most ∫_D 1/√(1+k²‖v‖²) + ε. (4) Product-cell statement: for h, M > 0, compact D with null boundary, v C¹ near D and M-hyperbolic on D, physicalRuled(h,D,v,M) has such an open-bounded cover of area at most h∫_D physicalWeight(h,v) + ε. (5) Orthogonal-grid statement: for compact D with null boundary, v C¹ near D, κ < 1, and at each point zero trace, negative determinant and derivative operator norm at most κ, physicalRuled(√2,D,v,1) has a parallelogram cover of area at most √2∫_D 1/√(1+v₁²+2v₂²) + ε. (6) Nilpotent statement: for compact D and G smooth (C^∞) near D whose derivative squares to zero at every point of D, and any h, ε > 0, there are finitely many square tiles T_i (congruent images of a scaled unit square) and directions g_i such that physicalRuled(1,D,G,1) lies in the union of the auxiliary cylinders {axial(s, b + s g_i)}, the sum of area(T_i)·physicalWeight(h,g_i) is at most ∫_D physicalWeight(h,G) + ε, and for every a there are two families of parallelogram cylinders, whose carriers are the images of these auxiliary cylinders under the two stated coordinate maps (a scaling by h in the third coordinate, and a coordinate swap with reflection a − z₃ scaled by h), each of area h·area(T_i)·physicalWeight(h,g_i). (7) Singular statement: for 1 < p < (√51 − 5)/2 and 1 < γ < 1/(2−p), an explicit coefficient (1/2)⁴(2p²+10p−13)/(30p) is negative, the explicit cost 2·singularCost + 8√2 c^{2γ} equals √2/2 + 2√2·coefficient·c² up to o(c²) as c → 0⁺, and for all sufficiently small c > 0 the regular edge-2 tetrahedron is covered by finitely many parallelogram cylinders covering two singular ruled pieces plus two triangular tip cylinders, with total area less than √2/2.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/RuledCovering.lean; bytes 9682..9723
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_RuledCovering

namespace OAI

noncomputable section

open Set MeasureTheory Filter

open scoped Topology ContDiff

namespace RuledApproximation

Formal statement
theorem fullMain : FullMain := by
  sorry

end RuledApproximation
end
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/RuledCovering.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

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 paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me