Good First Issues in Lean

Coordination issue: formalize low-rate capacity-achieving Reed–Solomon list decoding This is the source-of-truth issue for the project. Please claim a work package in a comment before starting, link every child issue and PR back here, and keep the dashboard below current. The intended unit of contribution is one narrow package with a frozen public interface, not one long-lived mega-branch. Summary Formalize Brakensiek–Chen–Putterman–Zhang–Zheng, Algorithmic List Decoding of Reed–Solomon Codes up to Capacity in the Low-Rate Regime (ECCC TR26-164, PDF). The paper gives a deterministic polynomial-time list decoder for every Reed–Solomon evaluation set over a prime field in the low constant-rate regime. Its new ingredient is a multivariate interpolant constrained by the values of hidden Hasse derivatives. A local rank bound makes the interpolation system small enough; Kopparty's differential-equation root finder turns the interpolant into a bounded candidate list. This is a

We should add an API-map for Lattice QFT including the main results that we would want to include there.

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/Relativity/Tensors/Elab.lean (around line 31) is incorrect. Current text Suppose `T2` is a tensor with color `![c3]`. Then `{T | μ ν ⊗ T2 | σ}ᵀ` is `prodNode (tensorNode T1) (tensorNode T2)`. Why this is wrong The documentation example claims that {T | μ ν ⊗ T2 | σ}ᵀ elaborates to prodNode (tensorNode T1) (tensorNode T2). This is incorrect because the preceding sentence introduces T, not T1, as the tensor with color ![c3]. The use of T1 refers to an undefined variable, while T is explicitly mentioned in the context. The correction replaces T1 with T, aligning the example with the declared tensor name. This matches the structure of other examples in the file, whi

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/QFT/PerturbationTheory/WickAlgebra/WicksTheorem.lean (around line 59) is incorrect. Current text 1. `timeOrder_eq_maxTimeField_mul_finset` is used to write `𝓣(φ₀…φₙ)` as `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ` Why this is wrong The documentation for the lemma timeOrder_eq_maxTimeField_mul_finset claims that 𝓣(φ₀…φₙ) is expressed using a term involving 𝓢(φᵢ, φ₀…φᵢ₋₁). This is incorrect because 𝓢 is not defined in the file and does not correspond to any standard notation in quantum field theory. In the context of time-ordered pr

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean (around line 21) is incorrect. Current text There are various properties which are preserved under this mapping: - Anomaly cancellation. - The presence of a specific term in the potential. - Being complete. Why this is wrong The documentation in physlib/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean incorrectly states that "anomaly cancellation" is preserved under the map function, but no lemma in the file supports this assertion. The module defines properties like map_allowsTerm and map_isComplete_iff, which correspond to the documented preservation of potential terms and completeness, respectively. However, ther

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/Relativity/Tensors/RealTensor/Basic.lean (around line 67) is incorrect. Current text /-- The tensor structure for complex Lorentz tensors. -/ Why this is wrong The docstring for realLorentzTensor incorrectly claims it defines "complex Lorentz tensors", but the declaration's name and surrounding context clearly indicate it is for real tensors. The file's comments explicitly mention "Real Lorentz tensors" and the definition uses Lorentz.ContrMod/Lorentz.CoMod, which are real vector spaces. This discrepancy arises because the docstring was not updated when the definition was renamed from a complex variant to a real one. The correction aligns the documentation with the actual purpo

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/SpaceAndTime/Space/Norm/Basic.lean (around line 15) is incorrect. Current text ## i. Overview The main content of this file is defining `Space.normPowerSeries`, a power series which is differentiable everywhere, and which tends to the norm in the limit as `n → ∞`. Why this is wrong The file claims that Space.normPowerSeries is a power series, but its definition as sqrt(‖x‖^2 + 1/(n+1)) does not match the mathematical definition of a power series (which is a sum of terms $a_k x^k$). The reviewer correctly notes this is a sequence of functions, not a power series. The correction accurately describes it as a sequence of functions that converges to the norm. This aligns wi

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean (around line 10) is incorrect. Current text # The MSSM with 3 families and RHNs We define the system of ACCs for the MSSM with 3 families and RHNs. We define the system of charges for 1-species. We prove some basic lemmas about them. Why this is wrong The file's documentation states it defines anomaly cancellation conditions for the MSSM with 3 families and right-handed neutrinos (RHNs). However, the code only implements charge definitions and ACCs for the standard MSSM without RHNs. The MSSMCharges structure and related lemmas like toSpecies split charges into SM fermions and MSSM Higgses but do not include any RHN

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it. Summary The documentation in Physlib/ClassicalMechanics/EulerLagrange.lean (around line 63) is incorrect. Current text - The variational derivative of `L t (q' t) (deriv q' t))` for a lagrangian `L` is equal to the `eulerLagrangeOp`. Why this is wrong The docstring for euler_lagrange_varGradient claims the variational derivative of L t (q' t) (deriv q' t) equals eulerLagrangeOp, but this is incorrect. The theorem actually proves that the variational derivative of the action functional — the integral of the Lagrangian over time — equals the Euler-Lagrange operator. The confusion arises because the docstring refers to the Lagrangian itself rather than its time integral, which is the correct object whose variatio

Binding in lambda calculi is notoriously prone to error, and isn't a problem where formalization is an immediate defense because this is a question of correct definitions. Especially because we will have multiple implementations of binding, I'd like to have a set of tests that give us a bit more confidence that we've written the correct definitions. I'd like to start with the existing locally nameless STLC and port something like what exists at https://github.com/sweirich/lambda-n-ways into a suite of tests. Help is welcome with this issue since I have somewhat limited time at the moment.

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. TauCeti/Analysis/Complex/Conformal/Reflection.lean carries the full pointwise Schwarz-reflection API (schwarzReflection, differentiableOn_conj_conj, eqOn_schwarzReflection_conj_of_real_on_axis, the upper/lower branch lemmas from five separate PRs) but never proves the theorem the file is named after: the ConformalMapping roadmap's L4 milestone, holomorphy of the reflected function across the real axis (DifferentiableOn ℂ F Ω on a symmetric domain, given holomorphy above, continuity up to the axis, and real boundary values). The hcont-style continuity hypothesis that the crossing argument needs is never used, and no Morera-type lemma exists anywhere in the directory. Task (new mathematics; cite TauCetiRoadmap/ConformalMapping/README.md L4 and match Suggested.lean's milestone signature; carry an authoring claim + tauceti-target ma

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. The ContourIntegration roadmap's distinctive layer, non-integer winding numbers for singularities on the contour (Hungerbühler-Wasem), exists only as definitions that nothing exercises: Analysis/Contour/RegularityConditions.lean's ConditionAprime, ConditionB, SectorCompatible, crossingAngle, basepointAngle, FlatOfOrder each appear in exactly one file (their own): zero consumers, zero instantiation lemmas, so their faithfulness to the paper is currently unfalsifiable. The only computed value is crossingAngle = π at a smooth crossing. ModelSectorWinding.lean's ½ and 1/6 "winding number" theorems evaluate (2πi)⁻¹ ∫ arc at the arc's centre, an off-curve point where the principal value is the ordinary integral; nothing yet computes a winding number to a non-integer value at an on-curve point. (These match the pinned Suggested.

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. Bernstein's theorem (a function on (0,∞) is completely monotone iff it is the Laplace transform of a unique finite measure) is close to assembled in TauCeti/Analysis/CompletelyMonotone/, but is never stated: BernsteinMeasures.lean (~1500 lines) carries the hard analytic content: the Chafaï approximation (chafaiRescaled, chafai_repeated_ibp, pointwiseBoundedOnUnitInterval) producing the approximating measures. Prokhorov/tightness machinery is available (the audit noted a Prokhorov.lean in the repo's dependency reach). BernsteinMeasures.lean's own docstring (around lines 22-24) defers "the final assembly ... recovering f itself" to "the Bernstein-theorem file", which does not exist. Task (new mathematics; cite TauCetiRoadmap/OneParameterSemigroups/README.md, the completely-monotone/Bernstein part, and carry an authoring claim +

From a whole-repo quality audit (2026-07-08, at d76e9fa). Verify each claim against current main before acting, and comment here if a claim no longer holds. ∂² = 0 for the fully blocked grid complex, the CombinatorialHeegaardFloer roadmap's designated first nontrivial theorem, is not yet proved. What exists: KnotTheory/Grid/DifferentialSquareCoefficient.lean reduces the goal: fullyBlockedDifferential_comp_self_eq_zero_iff (d² = 0 iff every length-two rectangle-count sum vanishes). DifferentialSquareSupport.lean bounds the support to two-step column-swap neighbours; card_fullyBlockedRectangles_le_two exists. The juxtaposition case analysis that discharges the sums (each composite domain decomposes as two empty rectangles in exactly two ways: disjoint, shared-corner, and the excluded annular cases, per Ozsváth-Stipsicz-Szabó's Grid Homology for Knots and Links) is absent. The files' own docstrings say "the statements here do not assert square-zero". Beware: SmallGridDifferential.l

What is the conjecture The Ramsey number $R(5,5)$ is defined as the smallest positive integer $n$ such that every 2-coloring of the edges of the complete graph $K_n$ contains either a monochromatic clique of 5 vertices or a monochromatic independent set of 5 vertices. Equivalently, for any graph $G$ on $n$ vertices, either $G$ or its complement $\overline{G}$ contains a clique of size 5. The exact value of $R(5,5)$ remains unknown, but it is bounded: $43 \leq R(5,5) \leq 48$. Also add conjectures for other small values. (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://oeis.org/A212954, https://mathworld.wolfram.com/RamseyNumber.html, https://gilkalai.wordpress.com/2017/03/29/r55-%E2%89%A4-48/, https://ajc.maths.uq.edu.au/pdf/5/ocr-ajc-v5-p13.pdf, https://math.mit.edu/~apost/courses/18.204_2018/ramsey-numbers.pdf Prerequisites needed Formalizability Rating: 1/5 (0 is best) (as of 2026-02-19) Bui

What is the conjecture The Van der Waerden number $W(r, k)$ is the smallest positive integer $n$ such that for every partition of the set ${1, 2, \ldots, n}$ into $r$ disjoint subsets, at least one subset contains an arithmetic progression of length $k$. The core open problem is to determine exact values of $W(r, k)$ for arbitrary pairs $(r, k)$. Known exact values are extremely rare: only the pairs $(2, 1), (2, 2), (2, 3), (2, 4), (2, 5), (2, 6), (3, 3), (4, 3), (5, 3), (6, 3), (2, 8), (3, 4)$ have been computed exactly. Computing even the next value remains an open computational challenge. Related open problems include improving upper and lower bounds for $W(r, k)$ and determining whether the mixed van der Waerden numbers are concave. (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: Wikipedia: Van der Waerden number Wolfram MathWorld: Van der Waerden Numbers Open Problem Garden: Concavity of van d

What is the conjecture Let $a_n$ denote the number of distinct flat foldings of a $1 \times n$ rectangular strip with horizontal and vertical creases marked as mountain or valley folds. The sequence ${a_n}$ (OEIS A000136) begins: $$a_1 = 1, \quad a_2 = 2, \quad a_3 = 6, \quad a_4 = 16, \quad a_5 = 50, \quad a_6 = 144, \quad a_7 = 462, \quad a_8 = 1392, \quad \ldots$$ The Growth Rate Conjecture: Determine the precise limiting ratio: $$\lim_{n \to \infty} \frac{a_{n+1}}{a_n}$$ It is known that this limit exists and lies in the interval $[3.3868, 3.9821]$, indicating exponential growth of $a_n$. However: The exact value of the limit remains unknown. It is unclear whether the limit has a closed form or is a transcendental number. Whether this limit can be expressed in terms of known mathematical constants is an open question. The similar problem for $2 \times n$ maps (OEIS A001415) also lacks a known growth rate formula. (This description may contain subtle errors especially on more comp

What is the conjecture For a positive integer $n$, define the aliquot sequence as the sequence $(s_0, s_1, s_2, \ldots)$ where $s_0 = n$ and $s_{i+1} = \sigma(s_i) - s_i$ for $i \geq 0$. Here $\sigma(m)$ denotes the sum of all positive divisors of $m$, and $\sigma(m) - m$ is the sum of proper divisors of $m$. The Catalan-Dickson conjecture states that every aliquot sequence is bounded. Specifically, every such sequence either terminates (reaches 1), reaches a perfect number (a number equal to the sum of its proper divisors), or enters a cycle of sociable numbers (numbers that are part of a periodic cycle under the aliquot iteration, including amicable pairs as special cases of length 2). (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: Wikipedia: Aliquot sequence Wolfram MathWorld: Catalan's Aliquot Sequence Conjecture ProofWiki: Catalan-Dickson Conjecture OEIS: Aliquot sequences Carl Pomerance: Ali

What is the conjecture A periodic group is a group in which every element has finite order. A finitely presented group is a group that can be described using a finite set of generators and finitely many relations between them. The conjecture asks: If $G$ is a finitely presented group and $G$ is periodic, must $G$ be finite? Equivalently: Does there exist a finitely presented group $G$ such that $G$ is periodic but $G$ is infinite? (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://en.wikipedia.org/wiki/Periodic_group, https://en.wikipedia.org/wiki/Presentation_of_a_group, Olshanskii, A. Yu. (1991). Geometry of defining relations in groups (Mathematics and Its Applications), Hall, M. (1959). The theory of groups (Macmillan) Prerequisites needed Formalizability Rating: 1.5/5 (0 is best) (as of 2026-02-03) Building blocks (1-3; from search results): Group and finite order concepts (via orderOf in M

What is the conjecture If $G$ is an edge-disjoint union of $n$ copies of the complete graph $K_n$, then the chromatic number $\chi(G) = n$. Here, an edge-disjoint union means the $n$ copies of $K_n$ share no common edges, and $\chi(G)$ is the minimum number of colors needed to color the vertices of $G$ such that no two adjacent vertices have the same color. (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://www.erdosproblems.com/19 Prerequisites needed Formalizability Rating: 1.5/5 (0 is best) (as of 2026-02-02) Building blocks (1-3; from search results): SimpleGraph type and basic graph operations in Mathlib CompleteGraph or ability to construct complete graphs Fintype for finite structures Missing pieces (exactly 2; unclear/absent from search results): Formal definition of chromatic number χ(G) and its properties Formalization of edge-disjoint union construction for graphs Rating justifica

What is the conjecture Define $h(n)$ as the largest $\ell$ such that there exists a sequence of primes $p_1 < \cdots < p_\ell$ all dividing $n$ where $p_{i+1} \equiv 1 \pmod{p_i}$ for each $i$. Define $H(n)$ as the largest $u$ such that there exists a sequence of integers $d_1 < \cdots < d_u$ all dividing $n$ where $d_{i+1} \equiv 1 \pmod{d_i}$ for each $i$. The open problems are: Estimate the growth rates of $h(n)$ and $H(n)$ as $n \to \infty$. Determine whether $H(n)/h(n) \to \infty$ for almost all $n$. Erdős conjectured that the typical order of $h(n)$ is the iterated logarithm $\log^*(n)$. (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://www.erdosproblems.com/696 Prerequisites needed Formalizability Rating: 2/5 (0 is best) (as of 2026-02-02) Building blocks (from Mathlib): Basic divisibility and modular arithmetic structures Prime factorization and divisor sequences Asymptot

What is the conjecture Let $f$ be a random completely multiplicative function on the positive integers, where for each prime $p$, we independently choose $f(p) \in {-1, 1}$ with equal probability. A function $f$ is completely multiplicative if $f(mn) = f(m)f(n)$ for all positive integers $m, n$. The conjecture asks whether with probability 1, $$\limsup_{N\to \infty}\frac{\sum_{m\leq N}f(m)}{\sqrt{N}}=\infty$$ (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://www.erdosproblems.com/1144 Prerequisites needed Formalizability Rating: 2/5 (0 is best) (as of 2026-02-01) Building blocks (1-3; from search results): Basic arithmetic and summation notation in Mathlib Probability theory foundations (probability spaces, independent random variables) Real analysis and limsup/liminf concepts Missing pieces (exactly 2; unclear/absent from search results): Formal definition and theory of multiplicative and co

What is the conjecture Let $f(z)$ be an entire function that is not a monomial. Define $\nu(r)$ as the number of points $z$ with $|z|=r$ where $|f(z)| = \max_{|z|=r}|f(z)|$ (which is finite for non-monomial entire functions). Question: Can $\liminf_{r \to \infty} \nu(r) = \infty$? Status: This is the second part of Erdős Problem 1117. The first part (whether $\limsup_{r \to \infty} \nu(r)=\infty$) was answered affirmatively by Herzog and Piranian. The second part remains open; Glücksam and Pardo-Simón have shown an "approximate" affirmative answer. (This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.) Sources: https://www.erdosproblems.com/1117 Prerequisites needed Formalizability Rating: 2/5 (0 is best) (as of 2026-02-01) Building blocks (1-3; from search results): Complex number absolute value and modulus properties Liminf and limsup of real-valued sequences Basic properties of entire functions (infinite diffe

The standard library has a tactic simp_to_model for proving facts about TreeMaps. We prove some facts about TreeMaps in HeapInstances.lean, but we do not make use of this automation yet. To make these proofs more robust, we should figure out how.