Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Quasi-isometric recognition of virtually polycyclic groups and solvable lattices

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorems selected for verification: OAI.PolycyclicRecognition.group_recognition OAI.PolycyclicRecognition.main_uniform_bounded_height OAI.PolycyclicRecognition.lattice_recognition

Lean statement file: PolycyclicRecognition.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 255 link it.

See the candidate theoremWho ran the proof-verification programReport a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem group_recognition    {P J : Type} [Group P] [Group J] [Group.FG P] [Group.FG J]    (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) :    IsVirtuallyPolycyclic J ∧      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by  sorrytheorem main_uniform_bounded_height    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)    (huni : ModelIsUnimodular R)    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]    (q : HeightSpace T.character ≃ₗ[ℝ] W)    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :    letI := d.compatibleMetrictheorem lattice_recognition    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)    (hΛ : IsFiniteCovolumeLattice Λ)    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • structure OAI.ChromaticCyclic.CyclicStep line 16

    structure CyclicStep {G : Type*} [Group G] (H K : Subgroup G) : Prop where  le : H ≤ K  normal : (H.subgroupOf K).Normal  cyclic : letI := normal; IsCyclic (K ⧸ H.subgroupOf K)

  • structure OAI.ChromaticCyclic.CyclicSeries line 21

    structure CyclicSeries {G : Type*} [Group G] (H K : Subgroup G) (n : ℕ) where  group : ℕ → Subgroup G  first : group 0 = H  last : group n = K  step : ∀ i < n, CyclicStep (group i) (group (i + 1))

  • definition OAI.PolycyclicRecognition.GroupBornologous line 39

    def GroupBornologous (f : G → H) : Prop :=  ∀ S : Set G, S.Finite → ∃ T : Set H, T.Finite ∧    ∀ x y, x⁻¹ * y ∈ S → (f x)⁻¹ * f y ∈ T

  • structure OAI.PolycyclicRecognition.GroupCoarseEquivalence line 44

    structure GroupCoarseEquivalence (G H : Type*) [Group G] [Group H] where  toFun : G → H  invFun : H → G  bornologous_toFun : GroupBornologous toFun  bornologous_invFun : GroupBornologous invFun  left_error : (Set.range fun x => x⁻¹ * invFun (toFun x)).Finite  right_error : (Set.range fun y => y⁻¹ * toFun (invFun y)).Finite

  • definition OAI.PolycyclicRecognition.IsPolycyclic line 61

    def IsPolycyclic : Prop :=  ∃ n : ℕ, Nonempty (CyclicSeries (⊥ : Subgroup G) ⊤ n)

  • definition OAI.PolycyclicRecognition.IsVirtuallyPolycyclic line 65

    def IsVirtuallyPolycyclic : Prop :=  ∃ H : Subgroup G, H.FiniteIndex ∧ IsPolycyclic H

  • definition OAI.PolycyclicRecognition.IsUniformLattice line 75

    def IsUniformLattice [TopologicalSpace G] (Λ : Subgroup G) : Prop :=  DiscreteTopology Λ ∧ ∃ K : Set G, IsCompact K ∧    ∀ g : G, ∃ (γ : Λ) (k : G), k ∈ K ∧ (γ : G) * k = g

  • structure OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel line 82

    structure SimplyConnectedSolvableLieModel where
    Show the remaining 13 lines
      modelSpace : Type  [normedAddCommGroup : NormedAddCommGroup modelSpace]  [normedSpace : NormedSpace ℝ modelSpace]  [finiteDimensional : FiniteDimensional ℝ modelSpace]  carrier : Type  [topologicalSpace : TopologicalSpace carrier]  [chartedSpace : ChartedSpace modelSpace carrier]  [group : Group carrier]  [lieGroup : LieGroup (𝓘(ℝ, modelSpace)) ⊤ carrier]  [t2Space : T2Space carrier]  [secondCountableTopology : SecondCountableTopology carrier]  [simplyConnectedSpace : SimplyConnectedSpace carrier]  [solvable : Group.IsSolvable carrier]

  • definition OAI.PolycyclicRecognition.IsFiniteCovolumeLattice line 106

    def IsFiniteCovolumeLattice {G : Type} [Group G] [TopologicalSpace G]    (Λ : Subgroup G) : Prop :=  letI : MeasurableSpace (G ⧸ Λ) := borel _  DiscreteTopology Λ ∧ ∃ μ : Measure (G ⧸ Λ),    IsProbabilityMeasure μ ∧ SMulInvariantMeasure G (G ⧸ Λ) μ

  • structure OAI.PolycyclicRecognition.LinearMetricChains line 113

    structure LinearMetricChains (X : Type*) [PseudoMetricSpace X] where  step : ℝ  step_pos : 0 < step  slope : ℝ  slope_nonneg : 0 ≤ slope  error : ℝ  error_nonneg : 0 ≤ error  chain : ∀ x y : X, ∃ (n : ℕ) (p : ℕ → X),    p 0 = x ∧ p n = y ∧ (n : ℝ) ≤ slope * dist x y + error ∧      ∀ i < n, dist (p i) (p (i + 1)) ≤ step

  • structure OAI.PolycyclicRecognition.ProperChainMetric line 125

    structure ProperChainMetric (G : Type*) [Group G] [TopologicalSpace G] where  metric : MetricSpace G  topology_eq : metric.toUniformSpace.toTopologicalSpace = ‹TopologicalSpace G›  proper : letI := metric; ProperSpace G  leftInvariant : letI := metric; IsIsometricSMul G G  chains : letI := metric; LinearMetricChains G

  • definition OAI.PolycyclicRecognition.heightKernel line 142

    def heightKernel (χ : I → L →ₗ[ℝ] ℝ) : Submodule ℝ L := ⨅ i, (χ i).ker

  • abbreviation OAI.PolycyclicRecognition.HeightSpace line 145

    abbrev HeightSpace (χ : I → L →ₗ[ℝ] ℝ) := L ⧸ heightKernel χ

  • definition OAI.PolycyclicRecognition.heightProjection line 148

    def heightProjection (χ : I → L →ₗ[ℝ] ℝ) : L →ₗ[ℝ] HeightSpace χ :=  (heightKernel χ).mkQ

  • structure OAI.PolycyclicRecognition.TriangularAdjoint line 154

    structure TriangularAdjoint (L : Type*) [LieRing L] [LieAlgebra ℝ L] (n : ℕ) where  basis : Basis (Fin n) ℝ L  upper : ∀ x : L, (LinearMap.toMatrix basis basis (LieAlgebra.ad ℝ L x)).IsUpperTriangular

  • definition OAI.PolycyclicRecognition.TriangularAdjoint.character line 164

    noncomputable def character (i : Fin n) : L →ₗ[ℝ] ℝ where  toFun x := T.basis.repr ⁅x, T.basis i⁆ i  map_add' x y := by simp [add_lie]  map_smul' r x := (by simp [smul_lie] : _ = r * T.basis.repr ⁅x, T.basis i⁆ i)

  • structure OAI.PolycyclicRecognition.IsGroupExponential line 181

    structure IsGroupExponential (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) : Prop where  map_zero : Exp 0 = 1  map_add_smul : ∀ (v : GroupLieAlgebra (𝓘(ℝ, E)) G) (s t : ℝ),    Exp ((s + t) • v) = Exp (s • v) * Exp (t • v)  hasMFDerivAt_zero : ∀ v : GroupLieAlgebra (𝓘(ℝ, E)) G,    HasMFDerivAt (𝓘(ℝ, ℝ)) (𝓘(ℝ, E)) (fun t : ℝ => Exp (t • v)) 0      (ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℝ ℝ) v)

  • definition OAI.PolycyclicRecognition.ModelIsUnimodular line 192

    def ModelIsUnimodular (R : SimplyConnectedSolvableLieModel) : Prop :=  letI : IsTopologicalGroup R.carrier :=    topologicalGroup_of_lieGroup (𝓘(ℝ, R.modelSpace)) ⊤  letI : LocallyCompactSpace R.carrier :=    Manifold.locallyCompact_of_finiteDimensional (𝓘(ℝ, R.modelSpace))  letI : MeasurableSpace R.carrier := borel _  letI : BorelSpace R.carrier := ⟨rfl⟩  (Measure.haar : Measure R.carrier).IsMulRightInvariant

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: bounded, connected, exponential, finite, fixed, group, height, invariant and ten more.

Theorem 1.4 of Quasi-isometric recognition of virtually polycyclic groups

Theorem (Uniform bounded height)

Let G be a connected simply connected real-triangulable unimodular Lie group, with a fixed left invariant Riemannian metric, exponential height map \pi:G\to W, and a fixed norm on W. There is a finite subgroup \A_G\leq\GL(W) such that, for every K\geq1 and C\geq0, there is a constant B=B(G,K,C) with the following property. Every (K,C) self quasi-isometry F of G has an A_F\in\A_G satisfying

\bigl\|\pi F(g)-\pi F(1)-A_F\pi(g)\bigr\|\leq B \qquad(g\in G).
Section 1, Introduction Read it in the paper TeX source, line 95
Show the TeX
Let $G$ be a connected simply connected real-triangulable unimodular Lie group, with a fixed left invariant Riemannian metric, exponential height map $\pi:G\to W$, and a fixed norm on $W$. There is a finite subgroup $\A_G\leq\GL(W)$ such that, for every $K\geq1$ and $C\geq0$, there is a constant $B=B(G,K,C)$ with the following property. Every $(K,C)$ self quasi-isometry $F$ of $G$ has an $A_F\in\A_G$ satisfying
\begin{equation}
 \bigl\|\pi F(g)-\pi F(1)-A_F\pi(g)\bigr\|\leq B
 \qquad(g\in G).
\end{equation}

Other possible paper matches, closest wording first

  • Proposition 11.3 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: kernel, locally, normal, real, virtually, unimodular and 16 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: generated and finitely.
  • Corollary 1.2 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: solvable, lattice, index, subgroup, isometric, connected and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: generated and finitely.
  • Theorem 1.1 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: polycyclic, virtually, isometric, group and quasi. Found in the paper’s title, which its main theorem states: recognition. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: generated and finitely.
  • Proposition 9.4 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: inverse, coarse, height, map, common, family and two more.
  • Proposition 8.3 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: difference, range, allowed, zero, steps, exp and seven more.
  • Corollary 5.7 of Quasi-isometric recognition of virtually polycyclic groups. Words of the Lean statement, its names split into words, that also appear in the theorem: represented, one, dist, continuous, exp, invariant and four more.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; Neal McBurnett’s openai-math-lean-tooling. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

  • Accepted Their term: “accepted”.

    Re-run through Comparator with Lean’s kernel: accepted (the check took 1804 s; peak memory 8.5 GiB).

    Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 255’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

  • MathVet

    Finds the whole advertised result stated or implied Their term: “full”.

    The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record

    Their note: group_recognition (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) [P, J f.g.] : IsVirtuallyPolycyclic J ∧ ∃ Γ finite-index, ∃ S Lie model, Λ, IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) and lattice_recognition (a finite-covolume lattice in a simply connected solvable Lie group, quasi-isometric to a f.g. J, makes J virtually a uniform lattice in possibly another such group). 'Quasi-isometric' is encoded as GroupCoarseEquivalence (bornologous maps with finite-set errors), which for f.g. groups is equivalent to a quasi-isometry; polycyclic = explicit cyclic subnormal series. Both summary claims are stated.

    Definitions the group asks readers to compare with the paper: Hand-built coarse geometry: GroupBornologous f := ∀ S finite, ∃ T finite, ∀ x y, x⁻¹ y ∈ S → (f x)⁻¹ (f y) ∈ T, GroupCoarseEquivalence (maps in both directions plus finite error sets) used instead of word-metric quasi-isometry; IsUniformLattice Λ := DiscreteTopology Λ ∧ ∃ K compact, ∀ g, ∃ γ k, k ∈ K ∧ γ k = g; SimplyConnectedSolvableLieModel packages Mathlib LieGroup/SimplyConnectedSpace/Group.IsSolvable. Plausible and standard but non-Mathlib. External package Gromov is in the import cone.

  • Carlos Toledo’s cert-machine

    Finds the whole advertised result stated or implied Their term: “MATCHES”.

    The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalization proves quasi-isometric recognition of virtually polycyclic groups: every finitely generated group quasi-isometric to a finitely generated virtually polycyclic group is itself virtually polycyclic. It also realizes a finite-index subgroup of the recognized group as a uniform lattice in a simply connected solvable Lie group, which may differ from the original ambient group.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

249 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 41 to its own declarations, 122 to Mathlib’s documentation. 23 declared names also link to the same declaration in OpenAI’s library. 1 identifier stays plain because it resolves to no single declaration: a variable Lean binds automatically, notation, or a name the scan of the pinned sources did not find. 1 of them could name more than one declaration. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAI/-! # Quasi-isometric recognition and uniform bounded heightA polycyclic group has a finite subnormal series with cyclic factors. Theheight quotient below is the quotient of the Lie algebra by the commonkernel of the diagonal adjoint characters.-/noncomputable sectionnamespace ChromaticCyclicstructure CyclicStep {G : Type*} [Group G] (H K : Subgroup G) : Prop where  le : H ≤ K  normal : (H.subgroupOf K).Normal  cyclic : letI := normal; IsCyclic (K ⧸ H.subgroupOf K)structure CyclicSeries {G : Type*} [Group G] (H K : Subgroup G) (n : ℕ) where  group : ℕ → Subgroup G  first : group 0 = H  last : group n = K  step : ∀ i < n, CyclicStep (group i) (group (i + 1))end ChromaticCyclicnamespace PolycyclicRecognitionopen Module LieAlgebra MeasureTheoryopen scoped Manifold NNRealsection Coarsevariable {G H J : Type*} [Group G] [Group H] [Group J]/-- Uniform control of finite sets of group differences. -/def GroupBornologous (f : G → H) : Prop :=  ∀ S : Set G, S.Finite → ∃ T : Set H, T.Finite ∧    ∀ x y, x⁻¹ * y ∈ S → (f x)⁻¹ * f y ∈ T/-- Coarse inverse maps with errors contained in fixed finite sets. -/structure GroupCoarseEquivalence (G H : Type*) [Group G] [Group H] where  toFun : G → H  invFun : H → G  bornologous_toFun : GroupBornologous toFun  bornologous_invFun : GroupBornologous invFun  left_error : (Set.range fun x => x⁻¹ * invFun (toFun x)).Finite  right_error : (Set.range fun y => y⁻¹ * toFun (invFun y)).Finiteend Coarsesection Polycyclicopen ChromaticCyclicvariable (G : Type*) [Group G]/-- Polycyclicity expressed by an actual cyclic subnormal series. -/def IsPolycyclic : Prop :=  ∃ n : ℕ, Nonempty (CyclicSeries (⊥ : Subgroup G) ⊤ n)/-- Virtual polycyclicity means a polycyclic subgroup of finite index. -/def IsVirtuallyPolycyclic : Prop :=  ∃ H : Subgroup G, H.FiniteIndex ∧ IsPolycyclic Hend Polycyclicsection UniformLatticevariable {G : Type*} [Group G]/-- A uniform lattice is discrete and has a compact fundamental cover. -/def IsUniformLattice [TopologicalSpace G] (Λ : Subgroup G) : Prop :=  DiscreteTopology Λ ∧ ∃ K : Set G, IsCompact K ∧    ∀ g : G, ∃ (γ : Λ) (k : G), k ∈ K ∧ (γ : G) * k = gend UniformLattice/-- A connected simply connected finite-dimensional real solvable Lie group. -/structure SimplyConnectedSolvableLieModel where  modelSpace : Type  [normedAddCommGroup : NormedAddCommGroup modelSpace]  [normedSpace : NormedSpace ℝ modelSpace]  [finiteDimensional : FiniteDimensional ℝ modelSpace]  carrier : Type  [topologicalSpace : TopologicalSpace carrier]  [chartedSpace : ChartedSpace modelSpace carrier]  [group : Group carrier]  [lieGroup : LieGroup (𝓘(ℝ, modelSpace)) ⊤ carrier]  [t2Space : T2Space carrier]  [secondCountableTopology : SecondCountableTopology carrier]  [simplyConnectedSpace : SimplyConnectedSpace carrier]  [solvable : Group.IsSolvable carrier]attribute [instance] SimplyConnectedSolvableLieModel.normedAddCommGroup  SimplyConnectedSolvableLieModel.normedSpace SimplyConnectedSolvableLieModel.finiteDimensional  SimplyConnectedSolvableLieModel.topologicalSpace SimplyConnectedSolvableLieModel.chartedSpace  SimplyConnectedSolvableLieModel.group SimplyConnectedSolvableLieModel.lieGroup  SimplyConnectedSolvableLieModel.t2Space SimplyConnectedSolvableLieModel.simplyConnectedSpace  SimplyConnectedSolvableLieModel.secondCountableTopology  SimplyConnectedSolvableLieModel.solvable/-- A discrete subgroup with a normalized invariant measure on its coset space. -/def IsFiniteCovolumeLattice {G : Type} [Group G] [TopologicalSpace G]    (Λ : Subgroup G) : Prop :=  letI : MeasurableSpace (G ⧸ Λ) := borel _  DiscreteTopology Λ ∧ ∃ μ : Measure (G ⧸ Λ),    IsProbabilityMeasure μ ∧ SMulInvariantMeasure G (G ⧸ Λ) μ/-- Explicit chains with bounded steps and a linear bound on their length. -/structure LinearMetricChains (X : Type*) [PseudoMetricSpace X] where  step : ℝ  step_pos : 0 < step  slope : ℝ  slope_nonneg : 0 ≤ slope  error : ℝ  error_nonneg : 0 ≤ error  chain : ∀ x y : X, ∃ (n : ℕ) (p : ℕ → X),    p 0 = x ∧ p n = y ∧ (n : ℝ) ≤ slope * dist x y + error ∧      ∀ i < n, dist (p i) (p (i + 1)) ≤ step/-- A compatible proper left-invariant metric with large-scale-geodesic chains. -/structure ProperChainMetric (G : Type*) [Group G] [TopologicalSpace G] where  metric : MetricSpace G  topology_eq : metric.toUniformSpace.toTopologicalSpace = ‹TopologicalSpace G›  proper : letI := metric; ProperSpace G  leftInvariant : letI := metric; IsIsometricSMul G G  chains : letI := metric; LinearMetricChains G/-- The compatible metric retains the original topology definitionally. -/abbrev ProperChainMetric.compatibleMetric    {G : Type*} [Group G] [TopologicalSpace G] (d : ProperChainMetric G) : MetricSpace G :=  d.metric.replaceTopology d.topology_eq.symmsection Heightvariable {L I : Type*} [AddCommGroup L] [Module ℝ L]/-- The common kernel, including the empty family of characters. -/def heightKernel (χ : I → L →ₗ[ℝ] ℝ) : Submodule ℝ L := ⨅ i, (χ i).ker/-- The canonical linear height quotient. -/abbrev HeightSpace (χ : I → L →ₗ[ℝ] ℝ) := L ⧸ heightKernel χ/-- The quotient map defining infinitesimal height. -/def heightProjection (χ : I → L →ₗ[ℝ] ℝ) : L →ₗ[ℝ] HeightSpace χ :=  (heightKernel χ).mkQend Height/-- A simultaneous real upper triangular basis for the adjoint representation. -/structure TriangularAdjoint (L : Type*) [LieRing L] [LieAlgebra ℝ L] (n : ℕ) where  basis : Basis (Fin n) ℝ L  upper : ∀ x : L, (LinearMap.toMatrix basis basis (LieAlgebra.ad ℝ L x)).IsUpperTriangularnamespace TriangularAdjointvariable {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n : ℕ}variable (T : TriangularAdjoint L n)/-- The diagonal entries of the adjoint representation. -/noncomputable def character (i : Fin n) : L →ₗ[ℝ] ℝ where  toFun x := T.basis.repr ⁅x, T.basis i⁆ i  map_add' x y := by simp [add_lie]  map_smul' r x := (by simp [smul_lie] : _ = r * T.basis.repr ⁅x, T.basis i⁆ i)end TriangularAdjointsection Exponentialattribute [local instance 10000] NormedField.toNormedSpacevariable {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]  [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]  [LieGroup (𝓘(ℝ, E)) ⊤ G]/-- The exponential is characterized by its one-parameter subgroups andby their tangent vectors at the identity. -/structure IsGroupExponential (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) : Prop where  map_zero : Exp 0 = 1  map_add_smul : ∀ (v : GroupLieAlgebra (𝓘(ℝ, E)) G) (s t : ℝ),    Exp ((s + t) • v) = Exp (s • v) * Exp (t • v)  hasMFDerivAt_zero : ∀ v : GroupLieAlgebra (𝓘(ℝ, E)) G,    HasMFDerivAt (𝓘(ℝ, ℝ)) (𝓘(ℝ, E)) (fun t : ℝ => Exp (t • v)) 0      (ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℝ ℝ) v)end Exponential/-- Unimodularity for the canonical Borel Haar measure of the Lie group. -/def ModelIsUnimodular (R : SimplyConnectedSolvableLieModel) : Prop :=  letI : IsTopologicalGroup R.carrier :=    topologicalGroup_of_lieGroup (𝓘(ℝ, R.modelSpace)) ⊤  letI : LocallyCompactSpace R.carrier :=    Manifold.locallyCompact_of_finiteDimensional (𝓘(ℝ, R.modelSpace))  letI : MeasurableSpace R.carrier := borel _  letI : BorelSpace R.carrier := ⟨rfl⟩  (Measure.haar : Measure R.carrier).IsMulRightInvariant/-- The upper, lower, and coarse-surjectivity bounds of a self quasi-isometry. -/structure SelfQuasiIsometry (G : Type*) [PseudoMetricSpace G] (K C : ℝ) where  toFun : G → G  upper : ∀ x y, dist (toFun x) (toFun y) ≤ K * dist x y + C  lower : ∀ x y, dist x y ≤ K * dist (toFun x) (toFun y) + K * C  surjective : ∀ y, ∃ x, dist y (toFun x) ≤ C/-- Quasi-isometric recognition, including the finite-index uniform-lattice realization. -/theorem group_recognition    {P J : Type} [Group P] [Group J] [Group.FG P] [Group.FG J]    (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) :    IsVirtuallyPolycyclic J ∧      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by  sorry/-- One finite slope group controls the height of every self quasi-isometry. -/theorem main_uniform_bounded_height    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)    (huni : ModelIsUnimodular R)    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]    (q : HeightSpace T.character ≃ₗ[ℝ] W)    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :    letI := d.compatibleMetric    ∃ A : Subgroup (W ≃ₗ[ℝ] W), Set.Finite (A : Set (W ≃ₗ[ℝ] W)) ∧      ∀ K C : ℝ, 1 ≤ K → 0 ≤ C → ∃ B : ℝ, 0 ≤ B ∧        ∀ F : SelfQuasiIsometry R.carrier K C, ∃ AF : A, ∀ g,          ‖(π (F.toFun g)).toAdd - ((π (F.toFun 1)).toAdd + AF.val (π g).toAdd)‖ ≤ B := by  sorry/-- Finite-covolume lattice recognition, allowing a different ambient Lie group. -/theorem lattice_recognition    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)    (hΛ : IsFiniteCovolumeLattice Λ)    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) := by  sorryend PolycyclicRecognitionendend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Quasi-isometric recognition of virtually polycyclic groups

Theorem

Let P be a finitely generated virtually polycyclic group, and let H be any finitely generated group. If H and P are quasi-isometric, then H is virtually polycyclic.

Section 1, Introduction Read it in the paper TeX source, line 10
Show the TeX
Let $P$ be a finitely generated virtually polycyclic group, and let $H$ be any finitely generated group. If $H$ and $P$ are quasi-isometric, then $H$ is virtually polycyclic.
Corollary

If a finitely generated group H is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of H is a uniform lattice in some connected simply connected solvable Lie group.

Section 1, Introduction Read it in the paper TeX source, line 18
Show the TeX
If a finitely generated group $H$ is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of $H$ is a uniform lattice in some connected simply connected solvable Lie group.
Theorem (Uniform bounded height)

Let G be a connected simply connected real-triangulable unimodular Lie group, with a fixed left invariant Riemannian metric, exponential height map \pi:G\to W, and a fixed norm on W. There is a finite subgroup \A_G\leq\GL(W) such that, for every K\geq1 and C\geq0, there is a constant B=B(G,K,C) with the following property. Every (K,C) self quasi-isometry F of G has an A_F\in\A_G satisfying

\bigl\|\pi F(g)-\pi F(1)-A_F\pi(g)\bigr\|\leq B \qquad(g\in G).
Section 1, Introduction Read it in the paper TeX source, line 95
Show the TeX
Let $G$ be a connected simply connected real-triangulable unimodular Lie group, with a fixed left invariant Riemannian metric, exponential height map $\pi:G\to W$, and a fixed norm on $W$. There is a finite subgroup $\A_G\leq\GL(W)$ such that, for every $K\geq1$ and $C\geq0$, there is a constant $B=B(G,K,C)$ with the following property. Every $(K,C)$ self quasi-isometry $F$ of $G$ has an $A_F\in\A_G$ satisfying
\begin{equation}
 \bigl\|\pi F(g)-\pi F(1)-A_F\pi(g)\bigr\|\leq B
 \qquad(g\in G).
\end{equation}
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 255 link it.
Solution module
OAI.GroupTheory.PolycyclicRecognition.Recognition
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
20 local vocabulary declarations
Lines of Lean, without comments or blank lines
136
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Quasi-isometric recognition of virtually polycyclic groups and solvable lattices

Family 255: Quasi-isometric recognition of virtually polycyclic groups

Candidate pairing

Theorem (Uniform bounded height)

Let G be a connected simply connected real-triangulable unimodular Lie group, with a fixed left invariant Riemannian metric, exponential height map \pi:G\to W, and a fixed norm on W. There is a finite subgroup \A_G\leq\GL(W) such that, for every K\geq1 and C\geq0, there is a constant B=B(G,K,C) with the following property. Every (K,C) self quasi-isometry F of G has an A_F\in\A_G satisfying

\bigl\|\pi F(g)-\pi F(1)-A_F\pi(g)\bigr\|\leq B \qquad(g\in G).

Quasi-isometric recognition of virtually polycyclic groups

TeX label thm:bounded-height, build/introduction.tex, line 95

The Lean statement says

theorem group_recognition    {P J : Type} [Group P] [Group J] [Group.FG P] [Group.FG J]    (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) :    IsVirtuallyPolycyclic J ∧      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by  sorrytheorem main_uniform_bounded_height    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)    (huni : ModelIsUnimodular R)    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]    (q : HeightSpace T.character ≃ₗ[ℝ] W)    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :    letI := d.compatibleMetric

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.two independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

20 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/PolycyclicRecognition.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Compare this statement with the paperShare a Comparator run reportSuggest a change