kim-em · Nov 1, 2026 · Nov 1, 2026
diff --git a/EvalTools/Markers.lean b/EvalTools/Markers.lean
@@ -1,8 +1,9 @@
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 import LeanEvalGenerator.Core.Markers
 
+-- The workspace generator drops Core.Markers and forwards other imports here.
+-- Keep marker implementation dependencies in Core.Markers so they do not leak
+-- into generated challenges.
+
 namespace EvalTools
 
 end EvalTools
diff --git a/LeanEval/GroupTheory/CommProbClosed.lean b/LeanEval/GroupTheory/CommProbClosed.lean
@@ -15,7 +15,7 @@ so there is no need to add in `0` to make the set of commuting probabilities clo
 
 /-- The set of commuting probabilities of finite groups is closed. -/
 @[eval_problem]
-theorem commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (hG : Group G), commProb G = p}) := by
+theorem commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (_hG : Group G), commProb G = p}) := by
   sorry
 
 end GroupTheory

diff --git a/generated/H1_not_closedComplemented/ChallengeDeps.lean b/generated/H1_not_closedComplemented/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.MeasureTheory.Function.L1Space.Integrable
 import Mathlib.Topology.Algebra.Module.Complement
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 namespace LeanEval
 namespace Analysis

diff --git a/generated/abel_ruffini/Challenge.lean b/generated/abel_ruffini/Challenge.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 open Polynomial
 

diff --git a/generated/abel_ruffini/Solution.lean b/generated/abel_ruffini/Solution.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 import Submission
 
 open Polynomial

diff --git a/generated/abel_ruffini/Submission.lean b/generated/abel_ruffini/Submission.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 import Submission.Helpers
 
 open Polynomial

diff --git a/generated/adoCharZero/ChallengeDeps.lean b/generated/adoCharZero/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 namespace LeanEval.RepresentationTheory.AdoIwasawa
 

diff --git a/generated/adoIwasawa/ChallengeDeps.lean b/generated/adoIwasawa/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 namespace LeanEval.RepresentationTheory.AdoIwasawa
 

diff --git a/generated/alternating_sign_matrix_count/ChallengeDeps.lean b/generated/alternating_sign_matrix_count/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 namespace LeanEval.Combinatorics.AlternatingSignMatrix
 

diff --git a/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean b/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Absolute profinite rigidity and hyperbolic geometry

diff --git a/generated/annals_algebraic_integers/ChallengeDeps.lean b/generated/annals_algebraic_integers/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.RingTheory.Algebraic.Defs
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Algebraic integers with conjugates in a prescribed distribution

diff --git a/generated/annals_bose_gases/ChallengeDeps.lean b/generated/annals_bose_gases/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Integral.Bochner.Basic
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from The energy of dilute Bose gases

diff --git a/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean b/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 import Mathlib.NumberTheory.ArithmeticFunction.Liouville
 import Mathlib.NumberTheory.DirichletCharacter.Basic
 import Mathlib.NumberTheory.SmoothNumbers
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from Higher uniformity of bounded multiplicative functions in short intervals

diff --git a/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean b/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Base
 import Mathlib.FieldTheory.Finite.GaloisField
 import Mathlib.RingTheory.Ideal.Norm.AbsNorm
 import Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from On the Chowla and twin primes conjectures over 𝔽_q[T]

diff --git a/generated/annals_conjecture_of_marton/ChallengeDeps.lean b/generated/annals_conjecture_of_marton/ChallengeDeps.lean
@@ -1,8 +1,5 @@
 import Mathlib.Algebra.Field.ZMod
 import Mathlib.Combinatorics.Additive.CovBySMul
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from On a conjecture of Marton

diff --git a/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean b/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.NumberTheory.LSeries.DirichletContinuation
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from The Weyl bound for Dirichlet L-functions of cube-free conductor

diff --git a/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean b/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Topology.MetricSpace.HausdorffDimension
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from On the Duffin-Schaeffer conjecture

diff --git a/generated/annals_enumerating_number_fields/ChallengeDeps.lean b/generated/annals_enumerating_number_fields/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Algebra.MvPolynomial.PDeriv
 import Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
 import Mathlib.NumberTheory.NumberField.Discriminant.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from Enumerating number fields

diff --git a/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean b/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.Normed.Algebra.Spectrum
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Equiangular lines with a fixed angle

diff --git a/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean b/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Order.Lattice.Nat
 import Mathlib.Data.Set.Card
 import Mathlib.Order.Filter.AtTopBot.Defs
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from A proof of the Erdős–Faber–Lovász conjecture

diff --git a/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean b/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Analysis.Complex.Exponential
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from A conjecture of Erdős, supersingular primes and short character sums

diff --git a/generated/annals_finite_time_singularity/ChallengeDeps.lean b/generated/annals_finite_time_singularity/ChallengeDeps.lean
@@ -4,9 +4,6 @@ import Mathlib.LinearAlgebra.CrossProduct
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 import Mathlib.Topology.MetricSpace.Holder
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Finite-time singularity formation for C^{1,α} solutions to

diff --git a/generated/annals_flat_littlewood_poly/ChallengeDeps.lean b/generated/annals_flat_littlewood_poly/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Algebra.Polynomial.Degree.Defs
 import Mathlib.Algebra.Polynomial.Eval.Defs
 import Mathlib.Analysis.Complex.Norm
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Flat Littlewood polynomials exist

diff --git a/generated/annals_fractal_uncertainty/ChallengeDeps.lean b/generated/annals_fractal_uncertainty/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Analysis.Fourier.LpSpace
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Fractal uncertainty in higher dimensions

diff --git a/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean b/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Probability.Distributions.SetBernoulli
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Thresholds versus fractional expectation-thresholds

diff --git a/generated/annals_good_lt_codes/ChallengeDeps.lean b/generated/annals_good_lt_codes/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.Algebra.Field.ZMod
 import Mathlib.InformationTheory.Hamming
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.Probability.ProbabilityMassFunction.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Good Locally Testable Codes

diff --git a/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean b/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.LinearAlgebra.Projectivization.Basic
 import Mathlib.NumberTheory.NumberField.AdeleRing
 import Mathlib.RingTheory.MvPolynomial.Homogeneous
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from The Hasse principle for random Fano hypersurfaces

diff --git a/generated/annals_hessian_estimates/ChallengeDeps.lean b/generated/annals_hessian_estimates/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.Analysis.InnerProductSpace.Spectrum
 import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 import Mathlib.MeasureTheory.Function.LpSeminorm.Defs
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Hessian estimates for the sigma-2 equation in dimension four

diff --git a/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean b/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Analysis.SpecialFunctions.Log.Base
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Improved bounds for the sunflower lemma

diff --git a/generated/annals_inscribed_rectangles/ChallengeDeps.lean b/generated/annals_inscribed_rectangles/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere
 import Mathlib.Geometry.Manifold.SmoothEmbedding
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 import Mathlib.Probability.Distributions.Fernique
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Inscribed rectangles in a smooth Jordan curve attain at least

diff --git a/generated/annals_integer_multiplication/ChallengeDeps.lean b/generated/annals_integer_multiplication/ChallengeDeps.lean
@@ -1,8 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Computability.TuringMachine.Computable
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Integer multiplication in time O(n log n)

diff --git a/generated/annals_large_value_estimates/ChallengeDeps.lean b/generated/annals_large_value_estimates/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from New large value estimates for Dirichlet polynomials

diff --git a/generated/annals_linear_subspaces/ChallengeDeps.lean b/generated/annals_linear_subspaces/ChallengeDeps.lean
@@ -2,9 +2,6 @@ import Mathlib.Algebra.Module.ZLattice.Basic
 import Mathlib.Analysis.InnerProductSpace.ExteriorPower
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
 import Mathlib.LinearAlgebra.Projectivization.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Rational approximations to linear subspaces

diff --git a/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean b/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.LinearAlgebra.Matrix.Permutation
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from The local-global conjecture for Apollonian circle packings is false

diff --git a/generated/annals_lorentzian_polynomials/ChallengeDeps.lean b/generated/annals_lorentzian_polynomials/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
 import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
 import Mathlib.RingTheory.MvPolynomial.EulerIdentity
 import Mathlib.Topology.Algebra.Module.ModuleTopology
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Lorentzian polynomials

diff --git a/generated/annals_mckay_conjecture/ChallengeDeps.lean b/generated/annals_mckay_conjecture/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Basic.Complex.Basic
 import Mathlib.GroupTheory.Sylow
 import Mathlib.RepresentationTheory.Character
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from The McKay Conjecture on character degrees

diff --git a/generated/annals_motivic_invariants/ChallengeDeps.lean b/generated/annals_motivic_invariants/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.AlgebraicGeometry.Birational.Composition
 import Mathlib.AlgebraicGeometry.Morphisms.Proper
 import Mathlib.Basic.Complex.Basic
 import Mathlib.NumberTheory.NumberField.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from Motivic invariants of birational maps

diff --git a/generated/annals_on_approximation_of_reals/ChallengeDeps.lean b/generated/annals_on_approximation_of_reals/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.RingTheory.Algebraic.Defs
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from On approximation to a real number by algebraic numbers of bounded degree

diff --git a/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean b/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean
@@ -1,8 +1,5 @@
 import Mathlib.Algebra.Module.FinitePresentation
 import Mathlib.GroupTheory.FinitelyPresentedGroup
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from On the coherence of one-relator groups and their group algebras

diff --git a/generated/annals_on_property_t/ChallengeDeps.lean b/generated/annals_on_property_t/ChallengeDeps.lean
@@ -3,9 +3,6 @@ import Mathlib.Algebra.MonoidAlgebra.MapDomain
 import Mathlib.Basic.Real.Basic
 import Mathlib.GroupTheory.FreeGroup.Basic
 import Mathlib.SetTheory.Cardinal.Finite
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from On property (T) for Aut(F_n) and SL_n(Z)

diff --git a/generated/annals_optimal_moebius/ChallengeDeps.lean b/generated/annals_optimal_moebius/ChallengeDeps.lean
@@ -1,8 +1,5 @@
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statement from The optimal paper Moebius band

diff --git a/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean b/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean
@@ -1,7 +1,4 @@
 import Mathlib.Algebra.Module.ZLattice.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from A counterexample to the periodic tiling conjecture

diff --git a/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean b/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean
@@ -1,9 +1,6 @@
 import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.Algebra.Polynomial.Degree.Defs
 import Mathlib.MeasureTheory.Function.LpSpace.Basic
-import Lake.Toml
-import Lake.Util.Message
-import Lean
 
 /-!
 # Main Statements from Pointwise ergodic theorems for non-conventional bilinear polynomial averages