Mathematical Contributions — KentaKitamura

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 📖 AI-contributions wiki entries matching these posts: 🟡 Partial result (Lean) alongside Hunter (2026), under “AI alongside literature” (21 Jun 2026), and ⚪ Candidate partial result (Lean) under “AI standalone” (23 Jun 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $N(k,\ell)$ be the minimal $N$ such that for any $f:\{1,\ldots,N\}\to\{-1,1\}$ there must exist a $k$-term arithmetic progression $P$ such that $ \left\lvert \sum_{n\in P}f(n)\right\rvert\geq \ell.$ Find good upper bounds for $N(k,\ell)$. Is it true that for any $c>0$ there exists some $C>1$ such that $N(k,ck)\leq C^k?$ What about $N(k,2)\leq C^k$ or $N(k,\sqrt{k})\leq C^k?$ — erdosproblems.com/176

• 2026-06-23 Lean formalization
  Lean 4 formalization of a polynomial upper bound for $N(k,\sqrt{k})$: for every $k\ge 2$, $N(k,\sqrt{k}) \le \lfloor \tfrac{4}{3}(k^2-k+1)(k-1)(k(k-1)+1)\rfloor + 1$, i.e. $N(k,\sqrt{k}) = O(k^5)$ — in particular an exponential-type bound $N(k,\sqrt{k})\le C^k$. Checked with no sorry/admit; axioms are the standard [propext, Classical.choice, Quot.sound].
  postGitHubLean4Web
• 2026-06-21 Lean formalization
  Lean 4 formalization of $N(k,2) \le \lfloor 2(k^2-1)(k-1)(2k+1)/(k-3)\rfloor + 1$ for $k\ge 5$ (an $O(k^3)$ bound), with the small cases $N(2,2)=3$, $N(3,2)=9$, $N(4,2)=13$ handled by finite Boolean checks — together giving the $C^k$-type upper bound for all $k\ge 2$.
  postGitHubLean4Web

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $k\geq 2$. Is it true that, for any distinct integers $1<n_1<\cdots <n_k$ such that $1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}$ we must have $\max(n_{i+1}-n_i)\geq 3$? — erdosproblems.com/287

• 2026-05-29 discussion
  Process note on how the successive bounds were found (interactive human+AI workflow: pointing the AI at unused information in the denominator sequence; the AI helped with algebra, arithmetic, drafting and verifier/search code).
  post
• 2026-05-28 bound + verified chain extension
  Finite strengthening of catsflowers5544's good-prime-chain certificate: any counterexample must have $k \ge 68634921076157089631$. Two improvements: a sharpened conversion from chain coverage to an $n_1$ lower bound, and a certified extension of the good-prime chain by safe-prime/Pocklington-certified primes up to $p_m = 147573952589666836319$ (giving $n_1 > 39943925344138028689$). Verifier/search scripts published.
  postGitHub
• 2026-05-28 bound
  Harmonic-sum corollary of the same certificate: any counterexample must have $k \ge 704390616921701072$ (from $n_1 > B = 409938931585744826$ and $1 = \sum 1/n_i < \log(1+k/B)$, so $k > (e-1)B$).
  post
• 2026-05-28 bound
  Combining the certificate with Woett's prime-power observation: any counterexample must have $k \ge 23$ (if $k\le 22$ then $n_1 \mid \mathrm{lcm}(1,\dots,42) = 219060189739591200$, contradicting the certificate). Rules out $k=19,\dots,22$ by a route different from the Lean verification of $k\le 18$.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $f(N)$ be the size of the largest $A\subseteq \{1,\ldots,N\}$ such that there are no solutions to $\frac{1}{a}= \frac{1}{b_1}+\cdots+\frac{1}{b_k}$ with distinct $a,b_1,\ldots,b_k\in A$? Estimate $f(N)$. In particular, is it true that $f(N)=(\tfrac{1}{2}+o(1))N$? — erdosproblems.com/301

• 2026-07-04 literature note
  Pointed out the preprint of Xinjun Wang, “A 667/806 Upper Bound for Erdős Problem #301 on Unit-Fraction-Free Sets” (May 2026): $f(N) \le (667/806 + o(1))N \approx 0.8275N$, improving the bound $25/28 \approx 0.8929$ recorded on the problem page (the conjectural $\tfrac12$ remains open).
  postpreprint
• 2026-07-04 observation
  Observation that Wang's $667/806$ configuration uses divisors of $720 = 2^4\cdot 3^2\cdot 5$, so a natural next finite experiment is to add the prime $7$.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $A=\{a_1<\cdots<a_k\}$ be a finite set of positive integers and extend it to an infinite sequence $\overline{A}=\{a_1<a_2<\cdots \}$ by defining $a_{n+1}$ for $n\geq k$ to be the least integer exceeding $a_n$ which is not of the form $a_i+a_j$ with $i,j\leq n$. Is it true that the sequence of differences $a_{m+1}-a_m$ is eventually periodic? — erdosproblems.com/341

• 2026-07-08 computation
  For the example $\{1,4,9,16,25\}$ the page says thousands of terms are needed before periodicity appears; under the stated Dickson rule (excluding sums $a_i+a_j$ with $i,j\le n$, $i=j$ allowed) the computation finds a period of length only 224: the periodic part starts at $a_{87}=440$ and $a_{n+224} = a_n + 1176$ for all $n \ge 87$. Reproducible Python check on Colab.
  postColab

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 📖 AI-contributions wiki listed under “AI collaborating with humans”: Kenta Kitamura — 🟢 Full solution (Lean) (21 Jun 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $A=\{1\leq a_1< a_2<\cdots\}$ be a set of integers such that $A\backslash B$ is complete for any finite subset $B$ and $A\backslash B$ is not complete for any infinite subset $B$. (Here 'complete' means all sufficiently large integers can be written as a sum of distinct members of the sequence.) Is it true that if $a_{n+1}/a_n \geq 1+\epsilon$ for some $\epsilon>0$ and all $n$ then $\lim_n \frac{a_{n+1}}{a_n}=\frac{1+\sqrt{5}}{2}?$ — erdosproblems.com/346

• 2026-06-21 Lean formalization
  Distinguished two readings of the problem (convergence-from-hypotheses vs. limit-exists). For the limit-exists interpretation, gave a Lean 4 formalization of an affirmative answer: if the two deletion hypotheses hold, the sequence has a uniform ratio gap, and $a_{n+1}/a_n \to L$ for some $L>1$, then $L = \varphi$. Axiom printout is the standard set, no sorryAx.
  postGitHubLean4Web

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Is there some $c>0$ such that every measurable $A\subseteq \mathbb{R}^2$ of measure $\geq c$ contains the vertices of a triangle of area 1? — erdosproblems.com/352

• 2026-06-03 method + code
  A finite upper-bound scheme for $f(N)$ in Koizumi's discrete $N$-avoiding lattice model: normalize a diameter pair, discard points by a triangle test, and bound the rest via chromatic numbers of compatibility graphs ($\omega \le \chi$), taking the max over branches and diameter vectors. Verified $f(N) \le 1,4,4,7,9,10,12$ for $N=1,\dots,7$ — matching the known lower-bound witnesses, so these small values are now exact.
  postGitHub
• 2026-05-31 witness repository
  Public repository of verified lower-bound witnesses for $N=1,\dots,40$ in Koizumi's model: $N\le 27$ from BorisAlexeev's posted witnesses (converted to uniform JSON and re-verified), $N=28,\dots,40$ new witnesses from own search; all checked by an exact integer verifier, with an interactive HTML viewer.
  postGitHubviewer
• 2026-05-31 theorem
  A sharp theorem for the low-side subproblem: if $F_{\mathrm{low}}(N)$ is the maximum size of $S\subseteq\mathbb{Z}^2$ all of whose triangles satisfy $\mathrm{area}+\mathrm{diam} < N$, then $F_{\mathrm{low}}(N) = (4\pi/\sqrt{27})N + O(\sqrt{N})$ — the disk constant $4\pi/\sqrt{27}$ is sharp. Proof via the Blaschke–Sas theorem and Pick's theorem.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Is it true that for every $k$ there are infinitely many primes $p$ such that the largest prime divisor of $\prod_{0\leq i\leq k}(p^2+i)$ is $p$? — erdosproblems.com/383

• 2026-06-21 computation
  Finite computational witness: the prime $p = 9188057$ satisfies $P^+\big(\prod_{0\le i\le k}(p^2+i)\big) = p$ for every $0 \le k \le 10$ (full factorizations given; $p^2+11$ breaks it). Search log over $p \le 10^7$: the number of primes surviving to $k = 1,2,\dots,10$ is $181281, 49789, 13811, 3229, 954, 227, 64, 13, 5, 1$, and none survive to $k=11$.
  post

• 🟢 Archived status OPEN — the 2026-07-09 Wayback snapshot records the problem as OPEN
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Is it true that for every $n\geq 1$ there is a $k$ such that $n(n+1)\cdots(n+k-1)\mid (n+k)\cdots(n+2k-1)?$ — erdosproblems.com/389

• 2026-08-01 computation
  Found explicit witnesses for $n=28,\ldots,33$: $(28,18253129921815)$, $(29,18253129921814)$, $(30,359503904702161)$, $(31,359503904702160)$, $(32,2394789405254690)$, and $(33,2394789405254689)$. For each pair $(n,k)$, the product of $n,\ldots,n+k-1$ divides the product of $n+k,\ldots,n+2k-1$. Since OEIS A375071 already gives exact minimal values through $n=27$, these witnesses extend verification of the existence assertion through $n=33$. The new values are upper-bound witnesses only; no minimality is claimed.
  postColab verificationOEIS A375071

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. For which integers $a\geq 1$ and primes $p$ is there a finite upper bound on those $k$ such that there are $a=a_1<\cdots<a_n$ with $p^k \mid (a_1!+\cdots+a_n!)?$ If $f(a,p)$ is the greatest such $k$, how does this function behave? Is there a prime $p$ and an infinite sequence $a_1<a_2<\cdots$ such that if $p^{m_k}$ is the highest power of $p$ dividing $\sum_{i\leq k}a_i!$ then $m_k\to \infty$? — erdosproblems.com/404

• 2026-07-08 witness repository
  Attempt repository for the odd-prime columns $p = 3,5,7,11,13$ of $f(a,p)$, with a clickable GitHub-Pages table of certificates. Contribution 1: baseline-case lower bounds $f(1,3), f(1,5), f(1,7) \ge 20000$ and $f(1,11), f(1,13) \ge 5000$ (finite witnesses, checked directly mod $p^K$) — in the direction of Terence Tao's comments about $f(1,5)$ in the thread. Contribution 2: exact rows such as $f(3,3)=3$, $f(39,3)=25$, $f(700,3)=363$, $f(110,5)=30$, $f(236,5)=61$, $f(42,7)=7$, $f(113,11)=11$, $f(163,13)=13$ (with small Lean4Web checks), plus scan-survivor lower-bound rows $f(a,p) \ge v_p(a!)$.
  postGitHubtable
• 2026-07-07 witness repository
  Repository of exact values in the $p=2$ column: $f(a,2)$ for $1 \le a \le 256$. Highlight: $f(2,2) = 254$ — the problem page records Lin's upper bound $f(2,2)\le 254$, and the repository supplies the matching lower-bound witness plus a two-sided Lean/Lean4Web check. For odd $a$ the value freezes at $f(a,2) = v_2(a!)$; for even $a$ cancellations make the landscape wild (largest value found: $f(34,2) = 18444$).
  postGitHubtableLean4Web

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. How many iterations of $n\mapsto \phi(n)+1$ are needed before a prime is reached? Can infinitely many $n$ reach the same prime? What is the density of $n$ which reach any fixed prime? — erdosproblems.com/409

• 2026-06-21 computation
  Explicit examples with $F(n) = 67$ (iterations of $n \mapsto \phi(n)+1$ to reach a prime): $2548851069$, $3398468092$, $5097702138$, all reaching the prime $9005041$ (full 67-step trajectory listed). Method: exhaustive totient-sieve sweep of $n \le 1.5\cdot 10^9$ (max found there: $F = 66$ at $n = 1371524731$), then a targeted inverse-totient extension from the high-$F$ frontier.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $F(n)$ be the maximum possible size of a subset $A\subseteq\{1,\ldots,N\}$ such that the products $ab$ are distinct for all $a<b$. Is there a constant $c$ such that $F(n)=\pi(n)+(c+o(1))n^{3/4}(\log n)^{-3/2}?$ If $A\subseteq \{1,\ldots,n\}$ is such that all products $a_1\cdots a_r$ are distinct for $a_1<\cdots <a_r$ then is it true that $\lvert A\rvert \leq \pi(n)+O(n^{\frac{r+1}{2r}})?$ — erdosproblems.com/425

• 2026-06-06 Lean formalization
  (Edited 2026-06-11 to link the complete Lean 4 formalization.) Lean 4 proof, assuming only PNT as a named hypothesis, that for every fixed $c < 3.499$ and all sufficiently large $n$: $F(n) \ge \pi(n) + c\,n^{3/4}(\log n)^{-3/2}$ — improving the previous lower coefficient $2.95$ from the thread. Construction upgrades the layered projective-plane approach: polarity graphs $ER_q$ on merged prime windows plus an averaging embedding using every layer pair under the hyperbola $pq\le n$; a uniform 20-band variant gives $C_{20} = 3.49901\ldots > 3.499$. Works in the stronger product-Sidon convention, hence implies the strict-pair version.
  postGitHubLean4Web
• 2026-06-06 proof (natural language)
  Natural-language proof that $\Lambda = 2^{11/4}/3^{3/4} = 2.9511517859\ldots$ is the exact supremum of the standard layered rectangular semiprime ansatz: every $\lambda < \Lambda$ is attainable and no $c > \Lambda$ is, via a Bellman-inequality certificate (Cauchy–Schwarz), maximized at cutoff $a_k = \sqrt{2/3}$. So beating $\Lambda$ requires leaving the rectangular layered ansatz (as the 3.499 construction above does).
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. What is the size of the largest $A\subseteq \mathbb{R}^d$ such that every three points from $A$ determine an isosceles triangle? That is, for any three points $x,y,z$ from $A$, at least two of the distances $\lvert x-y\rvert,\lvert y-z\rvert,\lvert x-z\rvert$ are equal. — erdosproblems.com/503

• 2026-05-29 observation
  Noted that in dimension $22$ one gets the exact value $f(22) = 276$: the Delsarte–Goethals–Seidel bound for spherical two-distance sets is tight in $\mathbb{R}^{22}$ (Musin), giving a spherical two-distance set of size $275$; adding the centre gives an isosceles set of size $276$, matching Blokhuis's general upper bound $f(22) \le \binom{24}{2} = 276$. (Also recorded as Corollary 6.4 in Chojecki's note.)
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 📖 AI-contributions wiki entry matching this post: 🟡 Partial result (Lean) under “AI standalone” (22 Jun 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $f(N)$ be the largest size of $A\subseteq \{1,\ldots,N\}$ with the property that there are no distinct $a,b,c\in A$ such that $[a,b]=[b,c]=[a,c],$ where $[a,b]$ denotes the least common multiple. Estimate $f(N)$ - in particular, is it true that $f(N)=o(N)$? — erdosproblems.com/536

• 2026-06-22 Lean formalization
  Lean 4 formalization of the upper bound $|A| \le N - \lfloor N/6 \rfloor = \lceil 5N/6 \rceil$ for $A \subseteq \{1,\dots,N\}$ with no three distinct $a,b,c$ satisfying $\mathrm{lcm}(a,b) = \mathrm{lcm}(a,c) = \mathrm{lcm}(b,c)$. Repository builds with lake build; no sorry/axiom/admit; standard axiom printout.
  postGitHubLean4Web

• ℹ️ Formalization of the resolution The problem was resolved by GPT 5.4 Pro (prompted by Chojecki), as credited in the page's remarks; these posts are Lean formalizations of the resolution material discussed in the thread, responding to the site's formalisation programme.
• 🟢 Badge history last archived as OPEN on 2026-01-13; marked SOLVED by 2026-07-09 — snapshot
• 📖 AI-contributions wiki this Lean formalization is listed under “Formalization” — of the Chojecki–GPT-5.4 Pro (2026) solution (17 May 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $(A_i)$ be a family of countably infinite sets such that $\lvert A_i\cap A_j\rvert \neq 2$ for all $i\neq j$. Find the smallest cardinal $C$ such that $\cup A_i$ can always be coloured with at most $C$ colours so that no $A_i$ is monochromatic. — erdosproblems.com/603

• 2026-05-17 Lean formalization
  Lean 4 / Mathlib formalization-attempt repository based on Chojecki's PDF and the thread discussion, covering two mathematical interpretations: the countable-sequence reading (find a finite colouring so no set is monochromatic) and the arbitrary-size-family reading (conditional on the Erdős–Rado partition relation, encoded as ArrowOmegaTwo κ μ). Both Lean4Web files linked.
  postGitHubLean4Web (1)Lean4Web (2)Chojecki PDF

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $\tau(n)$ count the number of divisors of $n$. Is there some $n>24$ such that $\max_{m<n}(m+\tau(m))\leq n+2?$ — erdosproblems.com/647

• 2026-05-29 observation
  Additional necessary condition on top of ScottHughes's reduction: any candidate $n > 84$ must satisfy $(n-3)/3$ prime — equivalently, the two prime-chain families acquire the extra conditions $(8s+5)/3$ prime and $(16s+5)/3$ prime. Proof: the candidate condition at $m = n-3$ forces $\tau(n-3) \le 5$; since $2520 \mid n$, write $n - 3 = 3r$ with $r > 27$; composite $r$ would give $\tau(3r) \ge 6$.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $A\subset\mathbb{N}$ be the set of $n$ such that for every prime $p\mid n$ there exists some $d\mid n$ with $d>1$ such that $d\equiv 1\pmod{p}$. Is it true that there exists some constant $c>0$ such that for all large $N$ $\frac{\lvert A\cap [1,N]\rvert}{N}=\exp(-(c+o(1))\sqrt{\log N}\log\log N).$ — erdosproblems.com/768

• 2026-07-09 literature note
  Pointed out the recent preprint of Eric Li, “The Sylow Divisor Condition: a Resolution of Erdős Problem 768”, which appears to settle the problem affirmatively: $|A\cap[1,x]|/x = \exp(-(c+o(1))\sqrt{\log x}\,\log\log x)$ with the explicit constant $c = 1/(2\sqrt{\log 2})$.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Does there exist a $k>2$ such that the $k$-sized subsets of $\{1,\ldots,2k\}$ can be coloured with $k+1$ colours such that for every $A\subset \{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$-sized subsets of $A$? — erdosproblems.com/835

• 2026-05-30 verification
  Independent verification (Hoffman ratio bound + Johnson-scheme eigenvalues, instead of edkirkby's Walsh–Hadamard idea) of the implication: if a proper $(k+1)$-colouring of $J(2k,k)$ exists in the remaining Ma–Tang cases (where $k+1$ is prime, $k$ even), then every colour class is closed under complementation — every $k$-set has the same colour as its complement. Uses equality analysis in Hoffman's bound and the Eberlein eigenvalue formula for the distance-$k$ graph.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $f_k(n)$ be the maximum possible chromatic number of a graph with $n$ vertices which contains no $K_k$. Is it true that, for $k\geq 4$, $f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}$ for some constant $c_k>0$? — erdosproblems.com/920

• 2026-06-30 status observation
  Observed that the #920 page already notes a positive answer to #986 implies a positive answer to #920, and #986 is now marked proved (following Bradač's off-diagonal Ramsey lower bound) — so #920 should now be positive / ready for a status update.
  post

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $r\geq 2$. An $r$-powerful number $n$ is one such that if $p\mid n$ then $p^r\mid n$. If $r\geq 4$ then can the sum of $r-2$ coprime $r$-powerful numbers ever be itself $r$-powerful? Are there at most finitely many such solutions? Are there infinitely many triples of coprime $3$-powerful numbers $a,b,c$ such that $a+b=c$? — erdosproblems.com/939

• 2026-05-25 computation
  For $r=5$, an explicit example not listed on the page: $2^5\cdot 17^6 + 7^{11} + 2^5\cdot 3^6\cdot 7^8 = 3^7\cdot 13^7$ (numerically $772402208 + 1977326743 + 134481277728 = 137231006679$; equivalently $17\cdot 34^5 + 7\cdot 49^5 + 1029\cdot 42^5 = 1521\cdot 39^5$). All four numbers are $5$-powerful and the three summands have joint gcd $1$ (not pairwise coprime). Appears smaller than the displayed $r=5$ example; reproducible verification published.
  postGitHub

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 📖 AI-contributions wiki this Lean formalization is listed under “Formalization” — of the GPT-5.5 Pro (2026) partial result (15 May 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $f(z)=\prod_{i=1}^n(z-z_i)\in \mathbb{C}[z]$ with $\lvert z_i\rvert \leq 1$ for all $i$. Let $\rho(f)$ be the radius of the largest disc which is contained in $\{z: \lvert f(z)\rvert< 1\}$. Determine the behaviour of $\rho(f)$. In particular, is it always true that $\rho(f)\gg 1/n$? — erdosproblems.com/1039

• 2026-05-15 Lean formalization
  Lean 4 / Mathlib formalization attempt of the proof strategy discussed in the thread, based on Liam Price's natural-language proof PDF.
  postGitHubLean4Web

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $k\geq 2$. Does there exist a prime $p$ and consecutive intervals $I_1,\ldots,I_k$ such that $\prod_{n\in I_i}n \equiv 1\pmod{p}$ for all $1\leq i\leq k$? — erdosproblems.com/1056

• 2026-06-21 witnesses
  Every $2 \le k \le 14$ has an explicit finite witness, extracted from OEIS A060427 and its b-file (following up StijnC's comment): for $p = 10428007$, fifteen listed factorials are all $\equiv 8978998 \pmod p$, so the fourteen adjacent intervals between them each have product $\equiv 1 \pmod p$. Primality and all fourteen interval products verified directly; the $k=14$ witness yields witnesses for every smaller $k$.
  postOEIS A060427

• ℹ️ Formalization of the resolution The problem page (last edited 2026-04-08, a month before the post) already recorded the resolution (the first part follows from Green–Tao; the second is answered by the standard mod-4 colouring). This post is a Lean formalization of that standard counterexample — the page's “results could be formalisable” list names KentaKitamura. No archive capture of the page predates 2026-07-09.
• 🔵 Status as of 2026-07-09 SOLVED — snapshot
• 📖 AI-contributions wiki this Lean formalization is listed under “Formalization” — second part, standard counterexample (12 May 2026) — wiki · archived snapshot
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $k\geq 3$. Is it true that, in any finite colouring of the integers, there are monochromatic arithmetic progressions of primes of length $k$? Are there monochromatic arithmetic progressions of length $k$ whose common difference is a prime? — erdosproblems.com/1187

• 2026-05-12 Lean formalization
  Formalized in Lean the standard mod-4 counterexample for the second part of the problem, with a Lean 4 Web typecheck.
  postGitHub

• 🟢 Status when posted OPEN — the 2026-07-09 snapshot of the problem page, taken after the posts below, still shows OPEN (statuses only move from open to solved)
• 💬 Comments on record archived thread · live thread · live problem page

Problem. Let $P_d(n)$ be such that in any set of $n$ points in $\mathbb{R}^d$ there exist at least $P_d(n)$ many points which do not contain an isosceles triangle. Estimate $P_d(n)$ - in particular, is it true that $P_2(n)<n^{1-c}$ for some constant $c>0$? — erdosproblems.com/1207

• 2026-07-08 literature note
  Pointed out the preprint of Lee–Pohoata–Zhu, “The Minkowski grid has robustly many repeated distances”, which appears to settle the conjectural part of the problem — the authors state their first result “confirms a conjecture of Erdős from 1980”.
  post

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted records WOWII Graph Conjecture 2 as research open with a sorry.
• 🔵 Current status SOLVED — Formal Conjectures PR #4654 was merged on 2026-08-08; mo271 approved and merged the independent proof contribution; the upstream entry now distinguishes three formal proofs and records this maximum-edge triangle-free-spanning-subgraph argument as the third.
• 🔗 Source problem Formal Conjectures: WOWII Graph Conjecture 2 (merged)

Problem. For every finite connected simple graph $G$, the maximum number $L_s(G)$ of leaves in a spanning tree satisfies $L_s(G) \ge 2\bigl(\overline{\alpha(N(v))}-1\bigr)$, where the barred term is the average, over vertices $v$, of the independence number of the subgraph induced by the neighbours of $v$. — Formal Conjectures: WOWII Graph Conjecture 2 (merged)

• 2026-07-27 formal conjectures submission
  Submitted Formal Conjectures PR #4654 with a complete Lean 4 proof of WOWII Graph Conjecture 2. The merged Formal Conjectures comment explicitly distinguishes three proofs: the first uses the methods of arXiv:2605.22763; the second combines a spanning-tree leaf bound from connected domination with ordered-pair double counting for adjacent neighbourhoods; and this independently developed contribution is the third. Its distinct argument chooses an edge-maximal triangle-free spanning subgraph, bounds each neighbourhood independence number by the corresponding degree, and uses the handshake lemma and Cauchy–Schwarz to find an edge with a large endpoint-degree sum. The resulting double star is extended to a spanning tree, whose leaf-count identity gives the required lower bound. The project contains no sorry, admit, native_decide, custom axiom, or unsafe declaration, and the axiom audit reports only propext, Classical.choice, and Quot.sound. A Formal Conjectures collaborator approved the contribution, and PR #4654 was merged on 2026-08-08.
  Formal Conjectures PR #4654 (merged)Formal Conjectures review approvalFormal Conjectures three-proof recordkernel-checked Lean proof (fixed commit)GitHubLean4Webearlier Formal Conjectures PR #4565
• 2026-08-08 formal proof merge
  Formal Conjectures collaborator mo271 approved the independent proof contribution with “Thanks, LGTM”, and PR #4654 was merged. The project now records this alternative argument as the third formal proof of WOWII Graph Conjecture 2 and describes its method separately from the two preceding proofs.
  review approvalPR #4654 (merged)merged Formal Conjectures source

• 🔵 Status when posted SOLVED — Formal Conjectures source at commit f7349f3 records the published result as research solved, while its Lean theorem body still ends in sorry.
• 🔗 Source problem Formal Conjectures: WOWII Graph Conjecture 31

Problem. Every finite connected simple graph $G$ contains an induced path on at least $2\,\operatorname{rad}(G)-1$ vertices; equivalently, $p(G) \ge 2\,\operatorname{rad}(G)-1$. — Formal Conjectures: WOWII Graph Conjecture 31

• 2026-07-28 formal conjectures submission
  Submitted Formal Conjectures PR #4658 with an immutable link to a complete Lean 4 formalization of the induced-path bound $p(G) \ge 2\,\operatorname{rad}(G)-1$. The artifact proves the exact assumptions and conclusion of the Formal Conjectures theorem and formalizes the argument in Theorem 2.2 of Erdős, Saks, and Sós (1986), where the proof is credited to Fan Chung. Both the local and Lean4Web versions contain no sorry or admit. This is a complete formalization of a published theorem, not a claim of a new mathematical proof.
  Formal Conjectures PR #4658kernel-checked Lean proof (fixed commit)GitHubLean4WebErdős–Saks–Sós (1986), Theorem 2.2

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 8bf45ed records WOWII Graph Conjecture 217 as research open with a sorry.
• 🔵 Current status SOLVED — Formal Conjectures PR #4656 was merged on 2026-08-04; Danie-I approved the complete external Lean proof and merged the status update into Formal Conjectures.
• 🔗 Source problem Formal Conjectures: WOWII Graph Conjecture 217 (merged)

Problem. Let $G$ be a finite connected simple graph. If $L_s(G) \le 4\,\mathbf{1}_{\operatorname{residue}(G)=2}+2$, where $L_s(G)$ is the maximum number of leaves among spanning trees of $G$, then $G$ has a Hamiltonian path. — Formal Conjectures: WOWII Graph Conjecture 217 (merged)

• 2026-07-28 formal conjectures submission
  Submitted Formal Conjectures PR #4656 with a complete Lean 4 proof of WOWII Graph Conjecture 217. When the graph residue is not $2$, the hypothesis reduces to $L_s(G)\le2$ and yields a Hamiltonian path directly. In the residue-$2$ case, $L_s(G)\le6$ bounds the maximum degree and the graph order; the proof applies a path form of Chvátal's condition or handles an explicit list of 39 exceptional degree sequences by structural graph arguments. The 118-module development and its approximately 49,000-line single-file audit contain no sorry or admit, use no LRAT/DRAT certificate, native_decide, or bv_decide, and report only propext, Classical.choice, and Quot.sound in the axiom audit.
  Formal Conjectures PR #4656 (merged)Formal Conjectures review approvalmerged Formal Conjectures sourcecanonical modular Lean proof (fixed commit)single-file kernel audit (fixed commit)GitHub
• 2026-08-04 formal proof merge
  Formal Conjectures collaborator Danie-I approved the complete Lean 4 proof contribution and merged PR #4656, changing WOWII Graph Conjecture 217 from research open to research solved and recording the immutable external proof.
  review approvalPR #4656 (merged)merged Formal Conjectures source

• 🟢 Status when posted OPEN — Formal Conjectures source at commit b2e608f records @[category research open, AMS 5] with a sorry.
• 🔵 Current status SOLVED — Formal Conjectures PR #4426 was merged on 2026-08-07; the upstream entry now says research solved and records the external proof as formal_proof using lean4.
• 🔗 Source problem Formal Conjectures: WOWII Graph Conjecture 316 (merged)

Problem. Let $G$ be a finite simple connected graph and let $P$ be its set of pendant vertices. If $|P|$ is at least the average degree of the complement of $G$, then $G$ is well totally dominated. — Formal Conjectures: WOWII Graph Conjecture 316 (merged)

• 2026-07-13 formal conjectures submission
  Submitted Formal Conjectures PR #4426 with a complete Lean 4 proof of WOWII Graph Conjecture 316, matching the theorem then recorded as research open. The project version was checked with Lean 4.27.0 and Mathlib v4.27.0 against Formal Conjectures commit b2e608f; the self-contained version also checks in Lean4Web. Both files compile without sorry, admit, or user-declared axioms, and the axiom printout is the standard [propext, Classical.choice, Quot.sound].
  Formal Conjectures PR #4426Formal Conjectures source when postedGitHubLean4Web
• 2026-08-07 formal proof merge
  After review, a Formal Conjectures reviewer accepted the complete Lean 4 proof contribution and PR #4426 was merged. The upstream entry now marks WOWII Graph Conjecture 316 as research solved and records the proof through the repository's formal_proof using lean4 mechanism.
  PR #4426 (merged)merged Formal Conjectures source

• 🔵 Status when posted SOLVED — Formal Conjectures PR #2177 source records Tao's 2017 theorem as research solved; this contribution formalizes the statement and definitions, not its proof.
• 🔗 Source problem Formal Conjectures: Lonely Runner, Tao (2017) variant (merged)

Problem. There exists an absolute constant $c>0$ such that, for all sufficiently large $n$, $\delta_n \ge 1/(2n)+c\log n/(n^2(\log\log n)^2)$. — Formal Conjectures: Lonely Runner, Tao (2017) variant (merged)

• 2026-02-06 formal conjectures statement submission
  Submitted Formal Conjectures PR #2177 adding the Tao (2017) variant of the Lonely Runner Conjecture. The contribution defines the unit circle $\mathbb{R}/\mathbb{Z}$, distance to the nearest integer, the maximal loneliness of an integer-velocity tuple, and the infimum $\delta_n$ over admissible tuples. It then states Tao's improved asymptotic lower bound $\delta_n \ge 1/(2n)+c\log n/(n^2(\log\log n)^2)$ for some $c>0$ and all sufficiently large $n$. This is a Lean formalization of a known theorem statement, not a formal proof of Tao's theorem.
  Formal Conjectures PR #2177 (merged)proposal issue #1935merged Formal Conjectures sourceTao (2017) paper
• 2026-05-06 statement merge
  Formal Conjectures collaborator Paul-Lez approved the revised statement with “LGTM”, and PR #2177 was merged into the upstream repository.
  PR #2177 (merged)merged commit

• 🟢 Status when posted OPEN — Formal Conjectures issue #3457 was open on 2026-07-13.
• 🔗 Source problem Open Quantum Problem #40

Problem. For positive semidefinite matrices $A,B$, let $p_{n,m}(A,B)$ be the normalized $t^n s^m$ coefficient of $\operatorname{tr}(tA+sB)^{n+m}$. Is it always true that $\operatorname{tr}(A^nB^m) \ge p_{n,m}(A,B) \ge \operatorname{tr}(\exp(n\log A+m\log B))$? — Open Quantum Problem #40

• 2026-07-13 literature note
  Pointed out the preprint of Hyunho Cha and Jungwoo Lee, “One-parameter counterexamples to the refined Bessis-Moussa-Villani conjecture” (March 2026), which gives a class of positive-semidefinite matrix counterexamples to the proposed upper bound $\operatorname{tr}(A^nB^m) \ge p_{n,m}(A,B)$. Moreover, the ratio $p_{n,m}(A,B)/\operatorname{tr}(A^nB^m)$ can be arbitrarily large. This falsifies the upper half of the two-sided refinement posed in Formal Conjectures issue #3457; it does not by itself settle the proposed exponential lower bound.
  postOpen Quantum Problem #40Formal Conjectures issue #3457arXiv:2603.19927PDF

• 🟢 Status when posted OPEN — Formal Conjectures PR #4644 submission explicitly proposes changing the Formal Conjectures entry from open to solved.
• 🔵 Current status SOLVED — Formal Conjectures PR #4644 was merged on 2026-08-04; the proof was validated by the MathOverflow asker, approved by a Formal Conjectures reviewer, and merged; the upstream entry now records the theorem as research solved.
• 🔗 Source problem Formal Conjectures: MathOverflow 507128 (merged)

Problem. There exist a commutative ring $R$ that is its own total quotient ring and a proper ideal $I\subsetneq R$ whose underlying $R$-module is invertible. — Formal Conjectures: MathOverflow 507128 (merged)

• 2026-07-27 formal conjectures submission
  Submitted Formal Conjectures PR #4644 with an explicit Lean 4 construction solving the exact target extracted from MathOverflow 507128. Let $D=\mathbb{C}[X,Y]/(Y^2-X^3)$ be the cuspidal-cubic coordinate ring and $P=(X-1,Y-1)$ its invertible ideal. The proof assembles a detector module from evaluation fibres away from the point corresponding to $P$, forms the idealization $R=D\ltimes M$, and takes the ideal induced by the multiplication map $R\otimes_D P\to R$. It proves that every nonunit of $R$ is a zero divisor, hence $R$ is its own total quotient ring, and proves that the induced ideal is both proper and invertible. The concrete algebraic input is constructed in Lean rather than assumed opaquely. The fixed proof contains no sorry or problem-specific axiom, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The MathOverflow question itself states that a proper invertible ideal in such an $R$ is equivalent to an infinite-order Picard class comparable to $[R]$. The asker subsequently published an answer identifying this construction as an independent solution.
  Formal Conjectures PR #4644 (merged)MathOverflow asker validationFormal Conjectures review approvalmerged Formal Conjectures sourcekernel-checked Lean proof (fixed commit)GitHubLean4WebMathOverflow question #507128MathOverflow answer by the asker
• 2026-08-04 formal proof merge
  The MathOverflow asker inspected the 735-line Lean4Web file and said it was fair to mark the problem formally solved. Formal Conjectures collaborator mo271 then approved the changes with “Thanks, LGTM!” and merged PR #4644.
  MathOverflow asker validationreview approvalPR #4644 (merged)merged Formal Conjectures source

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted records the Bézier–Bernstein target theorem as research open with an unspecified answer.
• 🔗 Source problem Formal Conjectures: Bézier–Bernstein Voronovskaja problem

Problem. Let $\alpha>0$ with $\alpha\ne1$, let $f$ be $C^2$ on $[0,1]$, and let $x\in[0,1]$. Then $\sqrt n\,(B_{n,\alpha}f(x)-f(x))$ converges to $\mu(\alpha)\sqrt{x(1-x)}\,f'(x)$, where $\mu(\alpha)=\int_0^\infty\bigl((1-\Phi(t))^\alpha-(1-\Phi(t)^\alpha)\bigr)\,dt$ and $\Phi$ is the standard normal distribution function. — Formal Conjectures: Bézier–Bernstein Voronovskaja problem

• 2026-07-27 formal conjectures submission
  Submitted Formal Conjectures PR #4646 with an explicit answer and a complete Lean 4 proof of the Bézier–Bernstein Voronovskaja problem. The proof constructs the powered-binomial probability law, proves its Gaussian-tail limit and uniform moment bounds, identifies the scaled first centered moment with $\mu(\alpha)\sqrt{x(1-x)}$, shows that the scaled second centered moment vanishes, and combines these facts with a uniform quadratic Taylor remainder. It also handles the endpoint cases $x=0$ and $x=1$. The original problem retains $\alpha\ne1$, although the formal argument works for every $\alpha>0$. The fixed proof contains no sorry or admit, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4646Formal Conjectures collaborator commentFormal Conjectures submission source (fixed head)kernel-checked Lean proof (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source at commit f7349f3 records the proposed universal upper bound as research open with a sorry.
• 🔗 Source problem Formal Conjectures: convex additive-VC₂ bound in ℝ³

Problem. Must every convex set $C \subseteq \mathbb{R}^3$ have additive $\mathrm{VC}_2$ dimension at most $1$? — Formal Conjectures: convex additive-VC₂ bound in ℝ³

• 2026-07-28 formal conjectures submission
  Submitted Formal Conjectures PR #4657 with an explicit counterexample to the claim that every convex subset of $\mathbb{R}^3$ has additive $\mathrm{VC}_2$ dimension at most $1$. The counterexample is a convex polyhedron cut out by six halfspaces with integer coefficients; a four-point $2\times2$ additive grid and sixteen explicit translations realize all sixteen membership patterns. The Lean 4 proof checks the certificate by exact arithmetic and has no sorry, admit, native_decide, custom axiom, or unsafe declaration; its axiom audit reports only propext, Classical.choice, and Quot.sound. A different 13-halfspace counterexample had previously appeared in closed draft fork PR #88, but its pinned Lean CI did not pass; the contribution here is the smaller six-halfspace construction and a completed kernel-checked formalization. PR #4657 also preserves the possible upper bound $2$ as a separate open statement.
  Formal Conjectures PR #4657kernel-checked Lean counterexample (fixed commit)GitHubLean4Webprior draft counterexample (fork PR #88)

• 🟢 Status when posted OPEN — Formal Conjectures source at commit f7349f3 records the six target integer declarations and their six trinary-integer counterparts as research open with answer(sorry).
• 🔗 Source problem Formal Conjectures: Monochromatic Quantum Graph integer cases

Problem. For every even $N \ge 6$ and every $D \ge 3$, the monochromatic quantum graph equation system has no solution with weights in $\mathbb{Z}$; consequently it has no solution when every weight is restricted to $\{-1,0,1\}$. — Formal Conjectures: Monochromatic Quantum Graph integer cases

• 2026-07-29 formal conjectures submission
  Submitted Formal Conjectures PR #4659 with a general Lean 4 theorem proving that for every even $N \ge 6$ and every $D \ge 3$, no integer-valued weighting satisfies the monochromatic quantum graph equation system. This settles all six integer declarations in the Formal Conjectures file, and the six declarations with weights restricted to $\{-1,0,1\}$ follow immediately. The proof uses no sorry, declared axiom, or native_decide; the wrapper axiom audit reports only propext, Classical.choice, and Quot.sound. The $N=6,D=3$ integer case and its trinary corollary overlap with PR #4511; the contribution here is the uniform all-even theorem.
  Formal Conjectures PR #4659twelve FC wrappers (fixed commit)GitHub

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 85f8637 records the three target declarations as research open with answer(sorry): the $N=6,D=5$ cases over $\mathbb{C}$ and $\mathbb{R}$, and the $N=10,D=9$ case over $\mathbb{C}$.
• 🔗 Source problem Formal Conjectures: Monochromatic Quantum Graph high-color cases

Problem. Over every commutative integral domain, any solution of the monochromatic quantum graph equation system on an even number $N \ge 6$ of vertices has at most $N-2$ colors. — Formal Conjectures: Monochromatic Quantum Graph high-color cases

• 2026-07-29 formal conjectures submission
  Submitted Formal Conjectures PR #4661 with a single solver-free Lean 4 theorem proving that every monochromatic quantum graph equation-system solution on an even number $N \ge 6$ of vertices over any commutative integral domain satisfies $D \le N-2$. This simultaneously proves nonexistence for $N=6,D=5$ over both $\mathbb{C}$ and $\mathbb{R}$ and for $N=10,D=9$ over $\mathbb{C}$, settling three declarations recorded as open. The proof uses no SAT solver, finite-classification certificate, native_decide, or sorry; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4661three FC wrappers (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 85f8637 records @[category research open, AMS 5 14 81] and answer(sorry).
• 🔗 Source problem Formal Conjectures: Monochromatic Quantum Graph (N=6, D=4)

Problem. For $N=6$ and $D=4$, does the monochromatic quantum graph equation system have no solution over $\mathbb{C}$? — Formal Conjectures: Monochromatic Quantum Graph (N=6, D=4)

• 2026-07-30 formal conjectures submission
  Submitted Formal Conjectures PR #4664 with a complete Lean 4 proof of eqSystem6_no_solution_d4, establishing that no weights $W : \mathrm{WeightsN}(6,4,\mathbb{C})$ satisfy the monochromatic quantum graph equation system. The formal result is stronger than the recorded complex case: it works over every commutative integral domain. The proof contains no sorry or admit, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The PR proposes changing the Formal Conjectures entry from answer(sorry) to answer(True) and recording the external Lean proof.
  Formal Conjectures PR #4664kernel-checked Lean proof (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 86db5cb records @[category research open, AMS 42 46] and answer(sorry).
• 🔗 Source problem Formal Conjectures: Weak Tiling Problem 4.3

Problem. Let $\Omega \subset \mathbb{R}$ be a finite union of intervals and let $\nu$ be a weak tiling measure for $\Omega$. Must $\nu$ be expressible as a convex combination of proper tiling measures? — Formal Conjectures: Weak Tiling Problem 4.3

• 2026-08-04 formal conjectures submission
  Submitted Formal Conjectures PR #4704 after an AI-assisted investigation found a counterexample to the statement recorded as Weak Tiling Problem 4.3. For $\Omega=(0,1)\cup(2,3)\cup(12,13)\cup(30,31)$, every convex combination of proper tiling measures assigns equal mass to $\{7\}$ and $\{15\}$, while the constructed weak tiling measure has masses $1/2$ and $0$, respectively. The linked Lean 4 development gives a complete kernel-checked proof with no sorryAx; #print axioms reports only propext, Classical.choice, and Quot.sound. The PR proposes changing the Formal Conjectures entry from answer(sorry) to answer(False) and marking it solved.
  Formal Conjectures PR #4704kernel-checked Lean proof (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 2270d31 records the constructive variant as @[category research open, AMS 5 11] with answer(sorry).
• 🔵 Current status SOLVED — Formal Conjectures PR #4853 was merged on 2026-08-10; reviewer mo271 approved the final revision; the upstream declaration now records research solved, answer(True), and the linked kernel-checked formal proof.
• 🔗 Source problem Formal Conjectures: Erdős #42 constructive variant (merged)

Problem. There exists a function $f:\mathbb{N}\to\mathbb{N}$ such that, whenever $M\ge1$ and $N\ge f(M)$, every maximal Sidon set $A\subseteq\{1,\ldots,N\}$ admits a Sidon set $B\subseteq\{1,\ldots,N\}$ of size $M$ whose difference set intersects $A-A$ only at $0$. — Formal Conjectures: Erdős #42 constructive variant (merged)

• 2026-08-10 formal conjectures submission
  Submitted Formal Conjectures PR #4853 with a complete Lean 4 proof of the constructive variant attached to Erdős Problem 42. The development imports Shashi456's formalization of the solved main Erdős #42 theorem, proves that its Sidon and maximal-Sidon predicates agree with the Formal Conjectures definitions, extracts a threshold for each $M$ from the Filter.atTop eventual statement, and uses classical choice to obtain the requested function $f$. This establishes existence of a threshold function; it does not compute an explicit numerical bound. The fixed proof contains no sorryAx, and #print axioms reports only propext, Classical.choice, and Quot.sound. During review, the proof metadata was updated to formal_proof using formal_conjectures and the dependency on Shashi456's main-theorem formalization was credited. Reviewer mo271 then approved the final revision, and PR #4853 was merged on 2026-08-10, changing the upstream declaration to research solved with answer(True).
  Formal Conjectures PR #4853reviewer approvalmerged Formal Conjectures commitkernel-checked Lean proof (fixed commit)main-theorem formalization dependencyGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 959255a marks the declaration research open, but quantifies over every planar set without a moving-sofa hypothesis.
• 🔗 Source problem Formal Conjectures: Wikipedia/MovingSofa before correction

Problem. For every set $s\subseteq\mathbb{R}^2$, is $\operatorname{sofaConstant}=\operatorname{volume}(s)$ equivalent to $s=\operatorname{gerversSofa}$? — Formal Conjectures: Wikipedia/MovingSofa before correction

• 2026-08-10 formal conjectures misformalization report
  Opened Formal Conjectures issue #4851 to show that the recorded uniqueness theorem was too broad: removing one point from Gerver's sofa gives a different planar set with the same area. This disproves the formal statement but not the intended moving-sofa uniqueness claim. William Blair then observed that merely adding a moving-sofa hypothesis would still leave translated copies as counterexamples, and authored PR #4852 to state uniqueness up to a rigid motion. The PR explicitly credits KitaKen1's point-removal counterexample, was approved by Formal Conjectures reviewer mo271, and was merged on 2026-08-10; issue #4851 was closed by the correction. The corrected conjecture itself remains research open.
  Formal Conjectures issue #4851original misformalized declarationcorrecting PR #4852reviewer approvalmerged correction commitlinked issue event

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 2270d31 labels W_3_20_lower through W_3_39_lower as research open and describes the bounds as conjectured.
• 🔗 Source problem Formal Conjectures: Green Problem 14 lower bounds

Problem. AKS14 establishes the twenty lower bounds for $W(3,t)$ recorded in Formal Conjectures for $20\le t\le39$, with finite good-partition certificates in Appendix A. For $20\le t\le30$ it separately conjectures equality with those bounds; for $31\le t\le39$ it states only lower bounds. — Formal Conjectures: Green Problem 14 lower bounds

• 2026-08-10 formal conjectures misformalization report
  Opened Formal Conjectures issue #4854 to document a mathematical-status error in Green Problem 14. The repository labels the twenty declarations W_3_20_lower through W_3_39_lower as research open and describes them as conjectured, whereas AKS14 presents all twenty inequalities as established lower bounds and supplies good-partition certificates in Appendix A. The report distinguishes these proved inequalities from the stronger exact-value conjectures: AKS14 conjectures equality only for $20\le t\le30$, while for $31\le t\le39$ it records further lower bounds without an equality conjecture. The proposed correction is therefore to mark the twenty lower-bound declarations research solved.
  Formal Conjectures issue #4854affected Formal Conjectures sourceAKS14

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 2270d31 marks the problem research open with answer(sorry), although Luo, Yang, and Zhu's paper proves that its answer is negative.
• 🔗 Source problem Formal Conjectures: Erdős Problem 973

Problem. Does there exist $C>1$ such that, for every $n≥2$, there are $z_1,…,z_n∈ℂ$ with $z_1=1$ and $|z_i|≥1$ for which $\max_{2\le k\le n+1}|\sum_i z_i^k|<C^{-n}$? — Formal Conjectures: Erdős Problem 973

• 2026-08-10 formal conjectures status-correction report
  Opened Formal Conjectures issue #4855 to report that Yanping Luo, Ruiyi Yang, and Keheng Zhu's paper Exterior power sums gives a negative answer to Erdős Problem 973. For every fixed $\lambda>0$ and all sufficiently large $n$, they prove that any $z_1,…,z_n∈ℂ$ with $|z_j|≥1$ satisfies $\max_{2\le k\le n+1}|\sum_j z_j^k|>e^{-\lambda n}$. Consequently, the $n$th root of the optimal maximum tends to 1, so no constant $C>1$ can satisfy the Formal Conjectures statement. The report proposes answer(False), research solved, and adding the paper to the references. The Lean development linked by the authors checks parts of the argument, not the full theorem.
  Formal Conjectures issue #4855affected Formal Conjectures sourceLuo–Yang–Zhu, Exterior power sumspartial Lean verification supplied by the authors

• 🟢 Status when posted OPEN — Formal Conjectures source at commit c252a41 marks both least-radius declarations research open with answer(sorry), while the definition of Circle permits negative radii.
• 🔗 Source problem Formal Conjectures: Wikipedia/SquarePacking

Problem. Do the sets of real radii admitting, respectively, a packing of three unit squares in $\operatorname{Circle}(r)$ and a packing of fifteen unit circles in $\operatorname{Circle}(r)$ have least elements? — Formal Conjectures: Wikipedia/SquarePacking

• 2026-08-10 formal conjectures misformalization report
  Opened Formal Conjectures issue #4859 to identify a shared flaw in least_three_square_packing_in_circle and least_fifteen_circle_packing_in_circle. Because Circle r is defined using only $r^2$, if $r>0$ then $\operatorname{Circle}(-r)=\operatorname{Circle}(r)$, so $-r$ is a smaller feasible radius. If $r\le0$, then $r^2<(r-1)^2$, hence $\operatorname{Circle}(r)\subseteq\operatorname{Circle}(r-1)$, and $r-1$ is smaller and feasible. Thus every feasible radius has a smaller one and neither formal set has a least element. This disproves only the misformalized statements, not the intended packing problems. The proposed repair is to require $0\le r$ or use $\mathbb{R}_{\ge0}$; the three square-container declarations are unaffected.
  Formal Conjectures issue #4859affected Circle definitionthree-square least-radius declarationfifteen-circle least-radius declaration

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 8adf5b7 marks both erdos_80 and erdos_80.variants.log as research open, while each quantifies over every real c > 0.
• 🔗 Source problem Formal Conjectures: Erdős Problem 80

Problem. For every real $c>0$, must the forced book size $f_c(n)$ eventually exceed $n^\varepsilon$ for some $\varepsilon>0$, or at least satisfy $f_c(n)\gg\log n$? — Formal Conjectures: Erdős Problem 80

• 2026-08-11 formal conjectures misformalization report
  Opened Formal Conjectures issue #4867 to identify a shared quantifier flaw in erdos_80 and erdos_80.variants.log. An admissible graph at density parameter $c$ must have at least $cn^2$ edges, but a simple graph on $n$ vertices has at most $n(n-1)/2$ edges. At $c=2$ no such graph exists for $n\ge1$, so the repository's empty-set convention gives $f(2,n)=0$. Consequently neither eventual lower bound by $n^\varepsilon$ nor domination of $\log n$ can hold for every $c>0$. This disproves only the over-quantified formal statements, not the intended Erdős problem. The report proposes restricting both declarations to the feasible range, for example $0<c<1/2$.
  Formal Conjectures issue #4867affected Formal Conjectures sourceoriginal Erdős Problem 80introducing PR #4830

• 🟢 Status when posted OPEN — Formal Conjectures source at commit 8adf5b7 records Fernandes Conjecture 1 as @[category research open, AMS 20].
• 🔗 Source problem Formal Conjectures: Fernandes Conjecture 1

Problem. For integers $m\ge n\ge2$ outside $(2,2),(3,3),(4,3),(4,4)$, the equal-sign subgroup $\Gamma_{m\oplus n}\le S_m\times S_n$ is generated by two elements. — Formal Conjectures: Fernandes Conjecture 1

• 2026-08-11 formal conjectures submission
  Submitted Formal Conjectures PR #4868 with a complete Lean 4 proof of Fernandes Conjecture 1. For each degree the proof constructs a transposition and an even permutation that generate the full symmetric group. For unequal degrees, paired generators give surjective coordinate projections; explicit powers and commutators place a three-cycle in the relevant Goursat kernel, so normality forces that kernel to contain the alternating group. The parity condition then yields the entire equal-sign subgroup. Equal degrees $m=n\ge5$ use a related pair whose square supplies the required three-cycle, and the low-degree cases are handled explicitly. The final audit checks the proved declaration and the Formal Conjectures declaration against the same proposition. The fixed proof contains no sorry or admit, uses neither native_decide nor bv_decide, and #print axioms reports only propext, Classical.choice, and Quot.sound. The PR proposes changing the upstream declaration from research open to research solved and attaching the fixed proof.
  Formal Conjectures PR #4868kernel-checked Lean proof (fixed commit)Fernandes (2026), arXiv:2605.12342GitHubLean4Web

• 🔵 Status when posted SOLVED — Grzesik–Hu–Volec (2016), p. 2 states immediately before Construction 2 that the Füredi–Maleki construction disproves Conjecture 1.1 for k=2, the C₅ case recorded as Erdős #608.
• 🔗 Source problem Erdős Problem 608

Problem. If $G$ has $n$ vertices and more than $n^2/4$ edges, must at least $2n^2/9$ edges of $G$ be contained in a $C_5$? — Erdős Problem 608

• 2026-08-11 formal conjectures literature/status report
  Posted a literature and status report in Formal Conjectures issue #824. The report identifies the exact passage in Grzesik–Hu–Volec (2016): the paragraph immediately before Construction 2 says that the Füredi–Maleki construction disproves Conjecture 1.1 for k=2, which is the C₅ case recorded as Erdős #608. It also links a complete external Lean 4/mathlib disproof published on 2026-07-29 by Emerson Hsieh (primateria), using a rational specialization of the Füredi–Maleki template and proving an explicit uniform gap below 2/9. The Lean proof is credited to its external author; this contribution is the evidence-backed literature and status report to Formal Conjectures, not a claim to either the original counterexample or its formalization.
  Formal Conjectures report in issue #824Grzesik–Hu–Volec (2016), p. 2arXiv abstractprimateria’s external Lean disproof (fixed commit)initial Lean disproof publication

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks sq_cube_root, sq_cube_root_isBigO, and limit as research open. The main Erdős #539 declaration and the Θ(√n) variants are separate and remain open.
• 🔵 Current status SOLVED — Formal Conjectures PR #4869 approval was merged on 2026-08-15; Formal Conjectures collaborator mo271 approved the contribution with “Thanks, nice!”. The merged source marks all three exponent-related variants research solved: the logarithmic exponent is 1/2, while the two proposed n^(2/3) statements have answer False. The main Erdős #539 declaration and the Θ(√n) variants remain open.
• 🔗 Source problem Formal Conjectures: Erdős Problem 539 variants (merged)

Problem. For the Formal Conjectures threshold $h(n)$ over $n$-element subsets of $\mathbb N$, determine $\lim \log h(n)/\log n$, and decide whether $n^{2/3}=O(h(n))$ and $h(n)=\Theta(n^{2/3})$. — Formal Conjectures: Erdős Problem 539 variants (merged)

• 2026-08-11 formal conjectures submission
  Submitted Formal Conjectures PR #4869 with complete Lean 4 proofs resolving three OPEN exponent-related variants of Erdős #539. Theorem A.1 of Schmitt et al. proves the exponent 1/2 for a threshold defined using finite sets of positive integers, whereas Formal Conjectures allows zero. The submitted bridge proves erdosH n ≤ cofactorThreshold (n+1) ≤ erdosH (n+1) and transfers the logarithmic limit by a squeeze argument. It then uses the limit to prove that n^(2/3) = O(cofactorThreshold n) is false and consequently that cofactorThreshold n = Θ(n^(2/3)) is false. The three exported declarations are checked against the corresponding Formal Conjectures propositions; the fixed proof contains no sorry or admit, and its axiom audit reports only propext, Classical.choice, and Quot.sound. This does not claim to resolve the main Erdős #539 problem or the Θ(√n) variants, which remain open.
  Formal Conjectures PR #4869 (merged)Formal Conjectures review approvalmerged Formal Conjectures sourcekernel-checked Lean proof (fixed commit)Schmitt et al. (2026), Theorem A.1ProofCouncil Lean source (fixed commit)original Erdős Problem 539GitHubLean4Web
• 2026-08-15 formal proof merge
  Formal Conjectures collaborator mo271 approved the complete Lean proof contribution with “Thanks, nice!”, and PR #4869 was merged. The upstream file now marks sq_cube_root, sq_cube_root_isBigO, and limit as research solved and links the fixed external proof; the main problem and Θ(√n) variants are still open.
  review approvalPR #4869 (merged)merged Formal Conjectures source

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks mathoverflow_10799.variants.kahn_kalai_conjecture_7 as research open with an unknown Boolean answer. The unconditioned and weak variants are separate.
• 🔵 Current status SOLVED — Formal Conjectures PR #4872 approval was merged on 2026-08-15; Formal Conjectures collaborator mo271 approved the status change and proof link with “Thanks, LGTM!”. The upstream entry now records the Diskin–Kreitner counterexample as research solved with answer(False), credits Sahar Diskin and Uri Kreitner for the counterexample, and credits Kenta Kitamura for adapting it to the exact Formal Conjectures statement and formalizing it in Lean.
• 🔗 Source problem Formal Conjectures: MathOverflow 10799, Kahn–Kalai variant (merged)

Problem. For every increasing family $F\subseteq2^{[n]}$, if $\mu_t(F)=1/2$ and $t/s>1000\log n$, must some $p\in[s,t]$ satisfy the Formal Conjectures optimality inequality? — Formal Conjectures: MathOverflow 10799, Kahn–Kalai variant (merged)

• 2026-08-11 formal conjectures submission
  Submitted Formal Conjectures PR #4872 with a complete Lean 4 disproof of the OPEN Kahn–Kalai Conjecture 7 variant registered under MathOverflow #10799. The mathematical counterexample is due to Sahar Diskin and Uri Kreitner; this contribution is an independent formalization, not the discovery of the counterexample. It constructs a scale-dense dual-tribes family whose members meet every block, proves the exact Bernoulli-measure and boundary identities, and chooses closely spaced block scales so that continuity gives μ_t(F)=1/2 and t/s > 1000 log n. At every p in [s,t], the normalized boundary is strictly too large for the Formal Conjectures IsOptimal inequality, so no required p exists. The repository proves both the literal negation of the fixed-1000 Formal Conjectures proposition and the original Kahn–Kalai Conjecture 7 quantifier pattern. The fixed proof contains no sorry, admit, custom axiom, or native_decide; #print axioms reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4872 (merged)Formal Conjectures review approvalmerged Formal Conjectures sourcekernel-checked Lean proof (fixed commit)Diskin–Kreitner counterexampleKahn–Kalai (2006), Conjecture 7MathOverflow #10799GitHubLean4Web
• 2026-08-15 formal proof merge
  Formal Conjectures collaborator mo271 approved the status change and external Lean proof with “Thanks, LGTM!”, and PR #4872 was merged. The merged source marks the variant research solved with answer(False), while preserving the distinction between Diskin and Kreitner's mathematical counterexample and Kenta Kitamura's adaptation and Lean formalization.
  review approvalPR #4872 (merged)merged Formal Conjectures source

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Roff–Willerton Conjecture 3.3 as research open with an unknown Boolean answer; only microscopic weighting ⇒ finite concentration was previously recorded as known.
• 🔗 Source problem Formal Conjectures: microscopic weighting conjecture

Problem. Does every nonempty finite metric space admit a microscopic weighting if and only if its distance matrix has finite concentration? — Formal Conjectures: microscopic weighting conjecture

• 2026-08-11 formal conjectures submission
  Submitted Formal Conjectures PR #4875 with a complete Lean 4 counterexample to the OPEN microscopic-weighting conjecture of Roff and Willerton. The proof constructs an explicit integral 10×10 distance matrix and checks symmetry, positive off-diagonal entries, and every triangle inequality. An explicit rational gauging proves finite concentration. For a kernel vector v with coordinate sum zero and A v = 0, the second-order expansion of Z(t) = exp(-tA) forces every possible microscopic limit g′ to satisfy vᵀ(A ∘ A)g′ = 0. A rational row-space certificate shows this quantity is unchanged across all gaugings, while the explicit gauging gives the nonzero value -103175560609824, yielding a contradiction. The analytic part also proves that the exponential similarity matrix is invertible for all sufficiently small positive t, so the inverse weighting used in the limit is the intended one. The fixed proof establishes the exact Formal Conjectures answer(False) proposition, contains no sorry, admit, or custom axiom, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4875kernel-checked Lean proof (fixed commit)Roff–Willerton (2026), Conjecture 3.3GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Green52.green_52_log as research open with an unknown Boolean answer. The qualitative O_K(1) statement Green52.green_52 is separate and remains open.
• 🔵 Current status SOLVED — Formal Conjectures PR #4887 was merged on 2026-08-12; reviewer mo271 approved the literature-backed Lean formalization, and PR #4887 was merged into Formal Conjectures. This closes only the logarithmic strengthening; the qualitative O_K(1) question remains open.
• 🔗 Source problem Formal Conjectures: Green Problem 52 logarithmic variant (merged)

Problem. If $A\subseteq\mathbb F_2^n$ has an additive complement of size $K$, must $2A$ contain a coset of codimension $O(\log K)$ with universal constants? — Formal Conjectures: Green Problem 52 logarithmic variant (merged)

• 2026-08-12 formal conjectures literature formalization submission
  Submitted Formal Conjectures PR #4887 to close the OPEN logarithmic strengthening of Green's Problem 52 by formalizing its known literature counterexample in Lean 4; reviewer mo271 approved the contribution and the PR was merged on 2026-08-12. Green's 2025 update credits Kaave Hosseini and Ryan Alweiss with independently observing that the logarithmic bound is too optimistic and records a Hamming-ball counterexample; this contribution is its formalization, not a claim to discovering the mathematical counterexample. For N = 2^(2t), the proof takes a Hamming ball of radius (N-2^t)/2 and uses Walsh characters, their complements, and Parseval's identity to construct an additive complement S with |S| ≤ 2N. Every vector in A+A has Hamming weight at most N-2^t, while a Lean-proved pivot-coordinate lemma forces any nonempty affine subspace of dimension d to contain a vector of weight at least d. Thus every affine subspace in A+A has codimension at least 2^t = √N, which eventually dominates C log |S| + D for all proposed universal real constants C,D. The fixed proof establishes the exact Formal Conjectures answer(False) proposition, contains no sorry, admit, custom axiom, native_decide, or unsafe theorem, and its axiom audit reports only propext, Classical.choice, and Quot.sound. It does not settle the first, qualitative O_K(1) question in Problem 52.
  Formal Conjectures PR #4887reviewer approvalmerged Formal Conjectures commitkernel-checked Lean proof (fixed commit)Green's Open Problems, Problem 52 and 2025 updateGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Erdos692.erdos_692.parts.ii as research open, but the declaration asks only for a maximizing endpoint to exist. The source problem asks where the maximum occurs; Part I is a separate declaration and was already marked solved.
• 🔗 Source problem Formal Conjectures: Erdős #692 maximum-existence variant

Problem. For fixed $n$, if $\delta_1(n,m)$ is the natural density of integers with exactly one divisor in $(n,m)$, does $\delta_1(n,m)$ attain a maximum as $m$ ranges over integers greater than $n+1$? — Formal Conjectures: Erdős #692 maximum-existence variant

• 2026-08-12 formal conjectures submission
  Submitted Formal Conjectures PR #4888 with a complete Lean 4 proof of the literal OPEN declaration associated with Part II of Erdős Problem 692. For fixed n, the proof first evaluates the base endpoint δ₁(n,n+2) = 1/(n+1). For all sufficiently large m, it places two disjoint finite blocks of primes inside (n,m) whose reciprocal sums are large. An integer having exactly one divisor in the interval cannot be divisible by primes from both blocks, so the density is bounded by the sum of two prime-avoidance densities and is strictly below the base value. Consequently every global maximizer lies in an explicit finite interval; a maximizing endpoint is then chosen from that finite set. This proves that a maximum is attained. The source problem asks where the maximum occurs, so this is a solved maximum-existence formal variant rather than a solution locating or characterizing a maximizing endpoint. It does not claim a closed formula or uniqueness. The fixed proof contains no sorry, admit, or custom axiom, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4888kernel-checked Lean proof (fixed commit)Formal Conjectures issue #4839Erdős Problem 692GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Erdos319.erdos_319.variants.isBigO as research open, but encodes no requirement that the supplied upper bound be simplest or optimal. The main problem and neighboring asymptotic variants are separate and remain unchanged.
• 🔗 Source problem Formal Conjectures: underformalized Erdős #319 Big-O variant

Problem. The docstring asks for the simplest $g(N)$ such that $c(N)=O(g(N))$, but the Lean declaration checks only that one supplied function is an upper bound; where is simplicity or optimality enforced? — Formal Conjectures: underformalized Erdős #319 Big-O variant

• 2026-08-12 formal conjectures misformalization report with lean witness
  Detected an underformalization in the OPEN isBigO variant of Erdős Problem 319. Its docstring asks for the simplest asymptotic upper bound, whereas its Lean proposition accepts any supplied function g for which c = O(g). PR #4890 demonstrated the gap with a kernel-checked witness g(N)=N: the IsGreatest hypothesis yields a maximizing set A ⊆ {1,…,N} with c(N)=|A|, so the ambient cardinality bound alone gives c(N)≤N. The signed reciprocal-sum condition is never used. Maintainer mo271 flagged the PR as a potential misformalization, and Issue #4892 was opened with the repository's misformalization label, proposing a matching lower bound or another explicit optimality condition. This is a valid elementary upper bound and a Lean witness to the statement flaw, not a solution of Erdős Problem 319. The fixed proof contains no sorry, admit, or custom axiom; its audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures misformalization issue #4892maintainer's misformalization observationFormal Conjectures PR #4890kernel-checked Lean proof (fixed commit)Erdős Problem 319GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Erdos357.erdos_357.parts.ii.bigO_version as research open with an answer hole. The central f(n)=o(n) problem, the other growth variants, and the weakly monotone variants are separate and remain unchanged.
• 🔗 Source problem Formal Conjectures: Erdős #357 lower Big-O variant

Problem. If $f(n)$ is the maximum length of a strictly increasing sequence in $[1,n]$ whose consecutive interval sums are all distinct, prove the explicit lower-growth answer $\sqrt n=O(f(n))$. — Formal Conjectures: Erdős #357 lower Big-O variant

• 2026-08-13 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4918 with a direct, kernel-checked Lean 4 proof for the OPEN lower Big-O answer hole attached to Erdős Problem 357. For r=⌊√n⌋, the proof uses the final r integers n-r+1,…,n. Intervals of different lengths have disjoint ranges of possible sums because r²≤n; intervals of the same length have equal sums only when they have the same starting point. Hence all consecutive interval sums are distinct and ⌊√n⌋≤f(n). The inequalities √n<⌊√n⌋+1≤2⌊√n⌋≤2f(n) then establish √n=O(f(n)) with constant 2. The proof is independent of the stronger Weisenberg lower bound already recorded in Formal Conjectures. Accordingly, this is a direct formal proof of a mathematically nontrivial registered variant, not a claim to a new lower bound or a solution of the central open question f(n)=o(n). It also leaves the upper Big-O, Big-Theta, little-o, infinite-density, reciprocal-sum, and weakly monotone declarations unchanged. The fixed proof contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4918kernel-checked Lean proof (fixed commit)direct construction and lower boundErdős Problem 357GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks the strict lower little-o target and the weakly monotone lower Big-O and little-o targets as research open, each with an answer hole. The central questions f(n)=o(n) and h(n)=o(n), the upper-growth and Big-Theta targets, and the infinite-sequence variants are separate and remain unchanged.
• 🔗 Source problem Formal Conjectures: Erdős #357 additional lower-growth variants

Problem. For the strict extremal function $f(n)$ and weakly monotone extremal function $h(n)$, prove the three registered targets $\log n=o(f(n))$, $\sqrt n=O(h(n))$, and $\log n=o(h(n))$. — Formal Conjectures: Erdős #357 additional lower-growth variants

• 2026-08-15 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4967 with kernel-checked Lean 4 proofs for three OPEN answer holes attached to Erdős Problem 357. The strict result combines the previously formalized direct bound √n=O(f(n)) with Mathlib's asymptotic relation log n=o(√n) to obtain log n=o(f(n)). For the weakly monotone formulation, the proof observes that admissibility already forces injectivity: singleton intervals with equal values would have equal sums. A monotone injective sequence in a linear order is strictly monotone, so the weak and strict extremal functions satisfy h(n)=f(n). Transferring the strict estimates then gives √n=O(h(n)) and log n=o(h(n)). This answers exactly the three named Formal Conjectures variants; it does not claim to solve Erdős Problem 357's central f(n)=o(n) question or its weakly monotone analogue. The fixed proof has no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4967three kernel-checked Lean proofs (fixed commit)strict lower little-o proofweakly monotone lower Big-O proofweakly monotone lower little-o proofearlier strict √n lower Big-O PR #4918Erdős Problem 357GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when reported marks Erdos688.erdos_688.parts.i.upper_bound as research open, but places no decay, sharpness, or nontriviality requirement on the comparison function supplied to the answer hole. The separate parts.ii declaration asks whether epsilonFunction=o(1).
• 🔗 Source problem Formal Conjectures: underformalized Erdős #688 upper-bound variant

Problem. The source asks for an upper estimate on $\epsilon_n$, in particular whether $\epsilon_n=o(1)$, but the Lean declaration accepts any $g$ satisfying $\epsilon=O(g)$. Why does the constant answer $g(n)=1$ count? — Formal Conjectures: underformalized Erdős #688 upper-bound variant

• 2026-08-13 formal conjectures misformalization report with lean witness
  Opened Formal Conjectures issue #4919, with the repository's misformalization label, to show that the OPEN upper-bound declaration for Erdős Problem 688 admits the trivial constant answer g(n)=1. For n≥2, applying a feasible covering to m=1 yields a prime with n^ε<p≤n; strict monotonicity of real powers gives ε<1. If the feasible exponent set is nonempty, exponent zero is feasible because every witness prime exceeds 1; if it is empty, Lean's totalized supremum is sSup ∅=0. Thus 0≤epsilonFunction(n)≤1 eventually, and the linked Lean4Web witness proves epsilonFunction=O(1). This bound neither estimates the decay or sharp order of epsilonFunction nor proves the separate conjecture epsilonFunction=o(1). The report therefore treats the proof as a concrete witness to a statement-design flaw, not as a solution of Erdős Problem 688, and proposes either fixing a meaningful target, explicitly requiring decay, or adding a warning that trivial answer instantiations must not trigger an open-to-solved status change.
  Formal Conjectures misformalization issue #4919interactive Lean witnessFormal Conjectures sourceErdős Problem 688introduction PR #3929

• 🟢 Status when posted OPEN — Formal Conjectures source when reported marks Erdos142.erdos_142.variants.upper as research open, but imposes no sublinearity, sharpness, or other nontriviality condition on the answer function. The main asymptotic-formula declaration and the neighboring variants remain separate.
• 🔗 Source problem Formal Conjectures: underformalized Erdős #142 upper-bound variant

Problem. The source asks for useful upper estimates or an asymptotic formula for $r_k(N)$, but the Lean declaration accepts any $g$ satisfying $r_k=O(g)$. Why does the ambient-set bound $g(N)=N$ count? — Formal Conjectures: underformalized Erdős #142 upper-bound variant

• 2026-08-13 formal conjectures misformalization report with lean witness
  Opened Formal Conjectures issue #4922, with the repository's misformalization label, to show that the OPEN one-sided upper-bound declaration for Erdős Problem 142 admits the trivial identity answer g(N)=N. Every admissible progression-free witness S is a subset of Finset.Icc 1 N, so |S|≤|Finset.Icc 1 N|=N; taking the supremal cardinality gives r(k,N)≤N for every k,N, and the linked kernel-checked Lean witness proves r_k=O(N) with Big-O constant 1. This uses no information about arithmetic-progression avoidance and supplies no nontrivial upper bound, order estimate, or asymptotic formula. The report therefore presents the proof as a concrete witness to a statement-design flaw, not as a solution of Erdős Problem 142. It proposes replacing the answer hole with fixed meaningful targets, adding an explicit warning against trivial answer instantiations, or encoding a genuinely sublinear requirement with the necessary condition on k. The issue also records that the standalone proof contains no sorry, admit, native_decide, or custom axiom, and its audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures misformalization issue #4922 and Lean4Web witnessFormal Conjectures sourceErdős Problem 142contribution guide on answer holesintroduction PR #555

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks both OeisA237271.conjecture_4 and OeisA237271.conjecture_5 as research open. The Carmichael-number observation is a separate declaration and remains unchanged.
• 🔗 Source problem Formal Conjectures: OEIS A237271 parity conjectures

Problem. For every positive $n$, prove that both $a(n^2)$ and $a(n(2n-1))$ are odd, where $a(N)$ counts the parts in the symmetric representation of $\sigma(N)$. — Formal Conjectures: OEIS A237271 parity conjectures

• 2026-08-13 formal conjectures literature-backed lean proof submission
  Submitted Formal Conjectures PR #4924 with kernel-checked Lean 4 proofs of the two OPEN parity declarations for OEIS A237271: a(n²) is odd and a(n(2n-1)) is odd for every positive n. The Formal Conjectures definition writes a(N) as one plus the number of adjacent divisor pairs (d,e) for which e is odd and 2d≤e. On adjacent pairs this condition is equivalent to the strict gap 2d<e; divisor complementation sends (d,e) to (N/e,N/d), preserves the gap, reverses the sorted divisor list, and is an involution. A fixed pair would satisfy de=N. For a square or a hexagonal number, the divisor n would then lie strictly between the paired divisors, contradicting adjacency. Thus the counted pairs occur in two-element orbits, their number is even, and the initial one makes a(N) odd. OEIS A237271 has recorded since 2021 that the parity of the sequence is the characteristic function of numbers with middle divisors; the contribution is a direct, self-contained Lean bridge to the current Formal Conjectures definitions, not a claim of a new mathematical discovery. It does not address the separate Carmichael-number declaration. The fixed proofs contain no sorry, admit, custom axiom, native_decide, or unsafe theorem; both axiom audits report only propext, Classical.choice, and Quot.sound. Formal Conjectures collaborator mo271 approved the submission on its first review, congratulated the resolution of the conjectures, enabled auto-merge, and placed the PR directly into the merge queue.
  Formal Conjectures PR #4924first-review approvalConjecture 4 Lean proof (fixed commit)Conjecture 5 Lean proof (fixed commit)OEIS A237271GitHubLean4Web
• 2026-08-13 first-review acceptance and automatic merge queue
  Formal Conjectures collaborator mo271 approved PR #4924 on the first review, writing “congrats on resolving the conjectures”. No revision was requested. The reviewer then enabled auto-merge and placed the PR directly into the merge queue.
  first-review approvalPR #4924

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks Zhi-Wei Sun's conjecture research open with a sorry, although the cited 2026 paper states that it proves exactly this representation theorem.
• 🔗 Source problem Formal Conjectures: OEIS A287616

Problem. Every nonnegative integer is representable as $x(x+1)/2+y(3y+1)/2+z(5z+1)/2$ for nonnegative integers $x,y,z$. — Formal Conjectures: OEIS A287616

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Cao, Guo, Qiu, Feng, and Gao's 2026 paper Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number settles the exact statement encoded by OeisA287616.conjecture. The paper's abstract explicitly says that it settles OEIS A287616, so the requested upstream action is to replace the open status with research solved and cite the result. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceCao–Guo–Qiu–Feng–Gao paperOEIS A287616

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks Green3.green_3 research open with an unknown Boolean answer, although a 2026 paper gives an affirmative solution.
• 🔗 Source problem Formal Conjectures: Green Problem 3

Problem. Every open $A\subseteq[0,1]$ of Lebesgue measure greater than $1/3$ contains $x,y,z\in A$ satisfying $xy=z$. — Formal Conjectures: Green Problem 3

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Franchi, Gowers, and Yip's 2026 paper Product-free subsets of (0,1) answers Green Problem 3 affirmatively: an open product-free subset of the unit interval has measure at most $1/3$. This is equivalent to the positive answer(True) requested by the Formal Conjectures declaration. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceFranchi–Gowers–Yip paper

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks both green_31.upper and green_31.variants.upper_eventually research open, while the reported 2026 bound has coefficient 0.9435.
• 🔗 Source problem Formal Conjectures: Green Problem 31 upper bounds

Problem. Improve the coefficient $0.98183$ in $F(N)\le\sqrt N+0.98183N^{1/4}+O(1)$, both infinitely often and eventually. — Formal Conjectures: Green Problem 31 upper bounds

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Hou and Zhao's 2026 paper Vector-valued smoothing for finite Sidon sets proves $F(N)\le\sqrt N+0.9435N^{1/4}+O(1)$. Since $0.9435<0.98183$ and the theorem holds eventually, it supplies a witness for the eventual declaration and hence also for the weaker infinitely-often declaration. The requested correction is to mark both upper-bound targets solved. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceHou–Zhao paper

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks both benchmark cases research open with unknown Boolean answers, although a 2026 classification proves existence for every local dimension d≥3.
• 🔗 Source problem Formal Conjectures: Open Quantum Problem 35 AME(7,d) cases

Problem. Do absolutely maximally entangled states AME(7,6) and AME(7,10) exist? — Formal Conjectures: Open Quantum Problem 35 AME(7,d) cases

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Shi, Zhang, Zhao, and Li's 2026 paper Complete Existence Classification of Seven-Partite Absolutely Maximally Entangled States proves that AME(7,d) exists exactly when $d\ge3$. The theorem directly gives positive answers to the Formal Conjectures benchmark cases AME(7,6) and AME(7,10). The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceShi–Zhang–Zhao–Li paper

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks the AME(12,5) benchmark research open with an unknown Boolean answer, although a 2026 construction proves existence.
• 🔗 Source problem Formal Conjectures: Open Quantum Problem 35 AME(12,5)

Problem. Does an absolutely maximally entangled state AME(12,5) exist? — Formal Conjectures: Open Quantum Problem 35 AME(12,5)

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Bevins and Bidav's 2026 paper Symmetry-guided constructions of absolutely maximally entangled states in five open cases constructs a Hermitian self-dual $[12,6,7]_{25}$ maximum-distance-separable code. Its stabilizer construction proves the existence of AME(12,5), giving the positive answer requested by the Formal Conjectures benchmark. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceBevins–Bidav paper

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks both parity cases research open, although Cho–Kim–Kim–Oum's Corollary 1.3 is reported to establish the displayed bounds.
• 🔗 Source problem Formal Conjectures: Independent Domination even and odd cases

Problem. For isolate-free graphs, prove the displayed even-degree bound $(D+2)^2i(G)\le(D^2+4)n$ and odd-degree bound $(D+1)(D+3)i(G)\le(D^2+3)n$. — Formal Conjectures: Independent Domination even and odd cases

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Cho, Kim, Kim, and Oum's paper Independent domination of graphs with bounded maximum degree, published in JCTB in 2023, supplies the even- and odd-maximum-degree bounds displayed in the two open Formal Conjectures declarations. The requested correction is to cite Corollary 1.3 and mark both declarations solved. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceCho–Kim–Kim–Oum paper

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks the universal statement research open, although a 2026 paper constructs an explicit pre-triangulated category that is not triangulated.
• 🔗 Source problem Formal Conjectures: MathOverflow 31809

Problem. Must every pre-triangulated category in the stated setting be triangulated? — Formal Conjectures: MathOverflow 31809

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Chen, Liu, Lu, and Zhang's 2026 paper A pre-triangulated category which is not triangulated constructs an explicit counterexample using finitely generated projective modules over the type-$A_5$ preprojective algebra over $\mathbb F_2$. This falsifies the universal proposition encoded in the Formal Conjectures declaration, so the proposed answer is False. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourceChen–Liu–Lu–Zhang paperMathOverflow question #31809

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks the lower and upper inequalities research open even though the same file already records the stronger solved identity C = 4.
• 🔗 Source problem Formal Conjectures: Green Problem 19 bounds

Problem. Prove the recorded bounds $C\ge3.13$ and $C\le4$ for the corner-density exponent. — Formal Conjectures: Green Problem 19 bounds

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that Green19.green_19 is already tagged research solved and states the exact identity $C=4$, while the immediately following weaker declarations $C\ge3.13$ and $C\le4$ remain tagged open. Both inequalities are direct consequences of the recorded exact value, so the report proposes correcting their status without making a new mathematical claim. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourcesame-file solved theorem C = 4

• 🟢 Status when posted OPEN — Formal Conjectures source at commit d16e05a marks the main asymptotic declaration research open, although the same file records Szabó's solved estimate with leading term N²/2 and lower-order error.
• 🔗 Source problem Formal Conjectures: Erdős Problem 272

Problem. Determine the main asymptotic of the largest family of subsets of $[N]$ whose pairwise intersections are nonempty arithmetic progressions. — Formal Conjectures: Erdős Problem 272

• 2026-08-13 formal conjectures literature-status report
  Reported in issue #4927 that the same Formal Conjectures file already tags Szabó's bound $t(N)=N^2/2+O(N^{5/3}\log^3N)$ as solved. Since the error term is $o(N^2)$, this directly implies $t(N)\sim N^2/2$, supplying the answer function for the still-open main asymptotic declaration. The stronger open question asking for an $O(N)$ error term is separate and is not claimed to be solved. The omnibus issue explicitly describes its list as AI-assisted and possibly mistaken; this entry therefore records a literature-status report pending Formal Conjectures maintainer verification, not an independent proof claim.
  Formal Conjectures issue #4927affected Formal Conjectures sourcesame-file solved Szabó bound

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Green37.green_37_littleO and Green37.green_37_bigO research open with unspecified answer functions. The exact, eventual-equality, and Theta declarations are separate and remain open.
• 🔗 Source problem Formal Conjectures: Green Problem 37 qualitative upper bounds

Problem. For each fixed $k$, let $m(N,k)$ be the minimum size of a set of natural numbers that contains a $k$-term arithmetic progression with common difference $d$ for every $1\le d\le N$. Prove $m(N,k)=o(N)$, and hence $m(N,k)=O(N)$. — Formal Conjectures: Green Problem 37 qualitative upper bounds

• 2026-08-14 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4943 with a complete Lean 4 proof of the two qualitative upper-bound declarations for Green Problem 37, using the explicit answer function N ↦ N. For a fixed progression length k, the construction chooses consecutive Fermat numbers as pairwise-coprime moduli. The Chinese remainder theorem assigns, for every difference d≤N, a start point whose jth progression term is divisible by the jth modulus. Taking the union of these sparse periodic residue classes inside a finite interval therefore supplies all required progressions. A cardinality bound makes the linear coefficient arbitrarily small by moving to sufficiently large Fermat moduli, proving $m(N,k)=o(N)$; the registered $O(N)$ theorem follows immediately. The fixed proof contains no sorryAx; its axiom audit reports only propext, Classical.choice, and Quot.sound. This closes only green_37_littleO and green_37_bigO. It does not determine the exact minimum, eventual formula, or Theta class, all of which remain open.
  Formal Conjectures PR #4943kernel-checked Lean proof (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Erdos361.erdos_361.asymptotic research open with an unspecified comparison function. The exact-value declaration Erdos361.erdos_361 is separate and remains open.
• 🔗 Source problem Formal Conjectures: Erdős #361 asymptotic variant

Problem. For fixed $c>0$, determine the order of growth of the maximum size of a set $A\subseteq\{1,\ldots,\lfloor cn floor\}$ for which no subset of $A$ sums to $n$. — Formal Conjectures: Erdős #361 asymptotic variant

• 2026-08-14 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4944 with a complete Lean 4 proof of the asymptotic variant of Erdős Problem 361, filling the answer with n ↦ n. The upper bound is the ambient-set estimate $|A|\le\lfloor cn floor$. For the lower bound, after choosing an integer k large enough in terms of c, the proof takes a block of consecutive integers immediately above $n/(k+1)$ and of length comparable to $n/(4k(k+1))$. A subset with at most k elements has sum below $n$, while one with at least k+1 elements has sum above $n$; hence the entire block avoids $n$ as a subset sum and gives a positive linear lower bound. Together these estimates prove that the extremal cardinality is $\Theta(n)$ for every fixed $c>0$. The fixed proof contains no sorryAx; its axiom audit reports only propext, Classical.choice, and Quot.sound. This solves only the registered asymptotic variant; it does not determine the exact extremal function or address its possible irregular dependence on $n$.
  Formal Conjectures PR #4944kernel-checked Lean proof (fixed commit)Erdős Problem 361GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures PR #4893 proposes the general theorem poissonNLie_of_scalarMatrix as research open; the PR itself remains open and has not yet been merged into Formal Conjectures.
• 🔗 Source problem Formal Conjectures PR #4893: proposed Poisson n-Lie target

Problem. Given a field $F$, a commutative $F$-algebra $A$, $n+m$ pairwise commuting derivations, and a scalar matrix $M\in M_{n+m,m}(F)$, prove that the determinant bracket formed from the derivative columns and the columns of $M$ satisfies the Poisson $n$-Lie identities encoded in Formal Conjectures PR #4893. — Formal Conjectures PR #4893: proposed Poisson n-Lie target

• 2026-08-14 independent lean proof publication
  Published a complete Lean 4 proof of the exact general target proposed in Formal Conjectures PR #4893 for the scalar-matrix determinant bracket associated with pairwise commuting derivations. The proof first establishes a stronger theorem for arbitrary natural numbers $n$ and $m$, so the registered hypotheses $n\ge2$ and $m\ge1$ are not needed. Alternation and the Leibniz rule follow from determinant identities. For the Filippov identity, the proof expresses the relevant Hamiltonian operator through adjugate cofactors, proves a Piola-type divergence cancellation, and cancels the mixed second-derivative terms using commutativity of the derivations and determinant antisymmetry. The fixed proof contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; both final declarations report only propext, Classical.choice, and Quot.sound. The exact Lean target is proved, but the source correspondence still needs review: the proposed IsPoissonNLie predicate does not state $F$-multilinearity, while the paper's Conjecture 3.5 cites additional assumptions that are absent from the Lean target. Accordingly, this record does not yet claim that every semantic detail of the paper conjecture has been captured.
  Formal Conjectures PR #4893kernel-checked Lean proof (fixed commit)Cao–Normatov–Omirov (2026), Conjecture 3.5GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA113019.conjecture as research open with an unknown Boolean answer; the OEIS entry itself asks whether 1 and 32 have any other fixed-point companions.
• 🔵 Current status SOLVED — OEIS A113019 revision #24 was approved and published on 2026-08-15; OEIS editor Alois P. Heinz approved the revision, and the public A113019 entry now states that 9^9 = 387420489 is also a fixed point, credited to Kenta Kitamura. This publishes the counterexample on OEIS; Formal Conjectures PR #4953 remains open separately.
• 🔗 Source problem Formal Conjectures: OEIS A113019 fixed-point conjecture

Problem. For $a(n)=(\text{number of decimal digits of }n)^{\operatorname{digitalRoot}(n)}$, are $1$ and $32$ the only fixed points? — Formal Conjectures: OEIS A113019 fixed-point conjecture

• 2026-08-15 formal conjectures counterexample submission
  Submitted Formal Conjectures PR #4953 with a concrete counterexample to the OPEN fixed-point question in OEIS A113019. For n = 387420489 = 9⁹, the decimal representation has nine digits and digit sum 45, hence digital root 9; therefore the sequence definition gives a(n) = 9⁹ = n. This is a third fixed point beyond 1 and 32, so the proposed classification is false. The Lean file proves both the explicit fixed-point identity and the exact Formal Conjectures target with answer(False). The proof uses simplification of the registered definition followed by arithmetic contradiction, contains no sorry or admit, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4953kernel-checked Lean proof (fixed commit)OEIS A113019OEIS approval revision #24GitHubLean4Web
• 2026-08-15 oeis update submission
  Submitted OEIS draft edit #18 adding the explicit fixed point 387420489 = 9⁹, the nine-digit and digital-root calculation, and attribution to Kenta Kitamura. Draft edit #19 then changed the draft status from editing to proposed. This records submission to OEIS, not editorial approval or publication.
  OEIS A113019 draftpublished OEIS A113019
• 2026-08-15 oeis publication
  After editorial compression of the submitted explanation, OEIS revision #24 was approved by Alois P. Heinz. The public entry now includes the comment “9^9 = 387420489 is also a fixed point,” with attribution to Kenta Kitamura, thereby publishing the counterexample and resolving the displayed fixed-point question. Formal Conjectures PR #4953 remains open as the separate Lean-status update.
  approved OEIS revision #24published OEIS A113019Formal Conjectures PR #4953

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA100478.conjecture as research open with an unknown Boolean answer. The registered target asks only for eventual periodicity, not eventual constancy or a classification of all cycles and limiting values.
• 🔗 Source problem Formal Conjectures: OEIS A100478 eventual-periodicity target

Problem. Given any five positive initial values, prove that the recurrence $a_{n+5}=\pi(a_n+a_{n+1}+a_{n+2}+a_{n+3}+a_{n+4})$ is eventually periodic. — Formal Conjectures: OEIS A100478 eventual-periodicity target

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4954 with a complete Lean 4 proof of the OPEN eventual-periodicity target associated with OEIS A100478. For initial maximum B, the proof sets t = B + 123 and K = 6006t. An elementary residue-class estimate for the prime-counting function gives π(30030t) ≤ 6006t, hence π(5K) ≤ K. Strong induction then shows that every term of the recurrence is at most K: whenever five consecutive terms lie below K, their sum is at most 5K and so is the next term. The five-term state therefore ranges over a finite set. Two states must coincide, and determinism of the recurrence propagates that equality to yield a positive eventual period. The core theorem is stronger than the registered target: it proves eventual periodicity for every nonnegative initial five-tuple, so the FC theorem does not use its positivity hypothesis. It does not claim that every orbit is eventually constant or classify the possible periods or constant values. The fixed proof contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its final axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4954kernel-checked Lean proof (fixed commit)OEIS A100478GitHubLean4Web
• 2026-08-15 oeis update submission
  Submitted OEIS draft edit #22 recording both the original all-ones orbit and the general theorem. Since a(54)=⋯=a(58)=66 and π(330)=66, the published sequence is constant at 66 from index 54 onward. More generally, the linked Lean proof establishes eventual periodicity for every five nonnegative initial values, ruling out the nonperiodic “third pattern” while leaving open whether every such orbit is eventually constant. The draft also adds the fixed-commit proof link and attribution to Kenta Kitamura. Draft edit #23 changed the state from editing to proposed; this records submission, not editorial approval or publication.
  OEIS A100478 draftpublished OEIS A100478fixed proof repository

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA108306.conjecture as research open; the corresponding OEIS comment presents the fully parameterized identity as a conjecture.
• 🔗 Source problem Formal Conjectures: OEIS A108306 INVERT–matrix conjecture

Problem. For arbitrary $a,b,n\in\mathbb N$, prove that the $n$-th term of the INVERT transform of $(1,a,ab,ab^2,ab^3,\ldots)$ equals the upper-left entry of $\begin{pmatrix}1&a\\1&b\end{pmatrix}^{n}$. — Formal Conjectures: OEIS A108306 INVERT–matrix conjecture

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4957 with a complete Lean 4 proof of the OPEN general identity attached to OEIS A108306. Writing D n for the INVERT transform, the proof introduces an auxiliary tail state T n and derives the simultaneous recurrences D(n+1)=D(n)+a·T(n) and T(n+1)=D(n)+b·T(n). These are exactly multiplication by the matrix [[1,a],[1,b]]. A simultaneous induction from the initial state (1,0) then identifies D n with the upper-left entry of the nth matrix power for every natural a, b, and n, proving the exact Formal Conjectures target. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound. The separate textbook theorem for the specialized sequence a=5, b=2 is outside this proof's claimed scope.
  Formal Conjectures PR #4957kernel-checked Lean proof (fixed commit)OEIS A108306GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA105801.conjecture as research open; OEIS attributes the conjecture to Giovanni Resta on 2010-11-17.
• 🔗 Source problem Formal Conjectures: OEIS A105801 modular-stabilization conjecture

Problem. For the Fibonacci–Collatz sequence $a(1)=1$, $a(2)=2$, with the next term equal to half the sum when it is even and three times the sum plus one when it is odd, prove that for every $k>0$ the sequence is eventually constant modulo $3^k$. — Formal Conjectures: OEIS A105801 modular-stabilization conjecture

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4959 with a complete Lean 4 proof of the OPEN conjecture attached to OEIS A105801. The proof transforms the sequence by y(n)=5a(n)+1. On consecutive transformed values, an even branch replaces the pair by its averaging step, whereas an odd branch triples their sum. Repeated averaging strictly decreases the gap between unequal same-parity entries until mixed parity is reached. From an odd–even pair, two consecutive triple branches produce three times another positive unequal pair. Since odd scaling commutes with both branches, this pumping argument iterates to reach a consecutive state divisible by 3^k for every positive k; that divisibility is then preserved by every later step. Thus 3^k eventually divides 5a(n)+1. Coprimality of 5 and 3^k forces all sufficiently late terms to have the same residue modulo 3^k, which is the exact Formal Conjectures target. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound. The same pumping theorem also applies mathematically to the related A181717 initial condition, but only the registered A105801 target is claimed as formalized here.
  Formal Conjectures PR #4959kernel-checked Lean proof (fixed commit)OEIS A105801GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA112970.conjecture1, conjecture2, and conjecture3 separately as research open; OEIS lists the corresponding identities together as conjectures.
• 🔗 Source problem Formal Conjectures: three OEIS A112970 conjectures

Problem. For the generalized Stern sequence satisfying $a(2r+1)=a(r)$, prove for every $n\in\mathbb N$ that $a(2^n)=a(2^{n+1}+1)$, $a(2^n-1)=a(3\cdot2^n-1)$, and $a(2^n-1)=1$. — Formal Conjectures: three OEIS A112970 conjectures

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4960 with complete Lean 4 proofs of all three OPEN targets attached to OEIS A112970. The proof first establishes the odd recurrence a(2r+1)=a(r) for the registered generalized Stern sequence, then iterates it to prove the stronger dyadic-ray lemma a(c·2^n−1)=a(c−1) for every c≥1 and natural n. The specializations c=1 and c=3 yield a(2^n−1)=1 and a(2^n−1)=a(3·2^n−1); a direct odd-recurrence step proves a(2^n)=a(2^(n+1)+1). The even recurrence is not needed. These are exactly the three Formal Conjectures declarations, but the separate OEIS identification a(2^n)=A033638(n) is not claimed as formalized. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; all three axiom audits report only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4960kernel-checked Lean proofs (fixed commit)OEIS A112970GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA113250.conjecture as research open; the A113250 OEIS entry presents the odd-index square property as a conjecture in the A113249 family.
• 🔗 Source problem Formal Conjectures: OEIS A113250 square-term conjecture

Problem. For the fourth-order integer recurrence corresponding to $m=4$ in the OEIS A113249 family, prove that every odd-indexed term $a(2n+1)$ is a perfect square. — Formal Conjectures: OEIS A113250 square-term conjecture

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4963 with a complete Lean 4 proof of the OPEN square-term conjecture for OEIS A113250, the m=4 specialization of the A113249 recurrence family. Setting p=m²=16, the shared proof defines a second-order sequence Y and proves the exact identity A(2n+1)=Y(n)². The odd subsequence of the fourth-order recurrence and the square sequence Y(n)² satisfy the same third-order linear recurrence, and their first three values agree; induction therefore proves that every odd-indexed term is an integer square. Specializing the parameterized theorem at p=16 proves the exact OeisA113250.conjecture target. A113250, A113252, and A113255 are recorded separately because they are distinct OEIS and Formal Conjectures entries, even though one family theorem proves all three. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4963kernel-checked Lean proof (fixed commit)OEIS A113250OEIS A113249 familyGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA113252.conjecture as research open; the A113252 OEIS entry presents the odd-index square property as a conjecture in the A113249 family.
• 🔗 Source problem Formal Conjectures: OEIS A113252 square-term conjecture

Problem. For the fourth-order integer recurrence corresponding to $m=6$ in the OEIS A113249 family, prove that every odd-indexed term $a(2n+1)$ is a perfect square. — Formal Conjectures: OEIS A113252 square-term conjecture

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4963 with a complete Lean 4 proof of the OPEN square-term conjecture for OEIS A113252, the m=6 specialization of the A113249 recurrence family. Setting p=m²=36, the shared proof defines a second-order sequence Y and proves the exact identity A(2n+1)=Y(n)². The odd subsequence of the fourth-order recurrence and the square sequence Y(n)² satisfy the same third-order linear recurrence, and their first three values agree; induction therefore proves that every odd-indexed term is an integer square. Specializing the parameterized theorem at p=36 proves the exact OeisA113252.conjecture target. A113250, A113252, and A113255 are recorded separately because they are distinct OEIS and Formal Conjectures entries, even though one family theorem proves all three. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4963kernel-checked Lean proof (fixed commit)OEIS A113252OEIS A113249 familyGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA113255.conjecture as research open; the A113255 OEIS entry presents the odd-index square property as a conjecture in the A113249 family.
• 🔗 Source problem Formal Conjectures: OEIS A113255 square-term conjecture

Problem. For the fourth-order integer recurrence corresponding to $m=9$ in the OEIS A113249 family, prove that every odd-indexed term $a(2n+1)$ is a perfect square. — Formal Conjectures: OEIS A113255 square-term conjecture

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4963 with a complete Lean 4 proof of the OPEN square-term conjecture for OEIS A113255, the m=9 specialization of the A113249 recurrence family. Setting p=m²=81, the shared proof defines a second-order sequence Y and proves the exact identity A(2n+1)=Y(n)². The odd subsequence of the fourth-order recurrence and the square sequence Y(n)² satisfy the same third-order linear recurrence, and their first three values agree; induction therefore proves that every odd-indexed term is an integer square. Specializing the parameterized theorem at p=81 proves the exact OeisA113255.conjecture target. A113250, A113252, and A113255 are recorded separately because they are distinct OEIS and Formal Conjectures entries, even though one family theorem proves all three. The proof is kernel checked and contains no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4963kernel-checked Lean proof (fixed commit)OEIS A113255OEIS A113249 familyGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA103425.conjecture as research open with answer(sorry); neither the OEIS question nor the registered target excludes constant or degenerate sequences.
• 🔗 Source problem Formal Conjectures: OEIS A103425 prime-free recurrence question

Problem. Do there exist relatively prime integer coefficients $(a,b,c)$ and an integer sequence satisfying $x_{n+3}=ax_{n+2}+bx_{n+1}+cx_n$ such that no $|x_n|$ is prime? — Formal Conjectures: OEIS A103425 prime-free recurrence question

• 2026-08-15 formal conjectures proof submission
  Submitted Formal Conjectures PR #4964 with an explicit Lean 4 witness answering the OPEN OEIS A103425 existence question affirmatively. Take coefficients (a,b,c)=(1,1,−1) and the constant sequence x(n)=4. The coefficients are relatively prime, the recurrence holds because 4=4+4−4, and every absolute term is 4, hence nonprime. This proves the exact registered statement with answer(True). The source and Formal Conjectures target do not require the sequence to be nonconstant, increasing, unbounded, or genuinely of minimal order three; this record therefore does not claim a proof of any such stronger nondegenerate variant. It also does not claim historical priority: Ivan Lunev published a stronger positive, nonconstant prime-free Tribonacci-like construction in 2017. The fixed Lean proof contains no sorry, admit, custom axiom, native_decide, or unsafe theorem, and its axiom audit reports only propext and Quot.sound.
  Formal Conjectures PR #4964kernel-checked Lean proof (fixed commit)OEIS A103425Lunev (2017), stronger nonconstant constructionGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA114831.conjecture3 as research open with a sorry. The four initial-value declarations in the file are tests, not additional open conjectures.
• 🔗 Source problem Formal Conjectures: OEIS A114831 asymptotic conjecture

Problem. Let $a(1)=1$, $a(2)=2$, and $a(n+1)=a(n)+\lfloor 2a(n)a(n-1)/(a(n)+a(n-1))\rfloor$. Prove that $a(n+1)/a(n)\to\sqrt3$. — Formal Conjectures: OEIS A114831 asymptotic conjecture

• 2026-08-15 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4969 with a kernel-checked Lean 4 proof of the OPEN asymptotic target for OEIS A114831. Writing r(n)=a(n+1)/a(n) and F(x)=1+2/(x+1), the floored recurrence gives r(n+1)=F(r(n))−e(n), where the nonnegative floor error tends to zero because the positive increasing sequence satisfies a(n)≥n. All relevant ratios lie in [1,3]; on this range, F has the positive fixed point √3 and contracts distance to it by a factor at most 1/2. A perturbed-contraction argument therefore proves r(n)→√3, exactly matching OeisA114831.conjecture3. This resolves the registered ratio-limit theorem but does not claim a closed formula or a sharper asymptotic expansion for a(n). The fixed proof has no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4969kernel-checked Lean proof (fixed commit)OEIS A114831GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA102371.conjecture as research open, with both answer(sorry) and a theorem-body sorry. The target includes the necessary condition 0<n.
• 🔗 Source problem Formal Conjectures: OEIS A102371 identity

Problem. For every $n\ge1$, prove that the OEIS A102371 term satisfies $a(n)=2^n-1-\operatorname{A105033}(n-1)$. — Formal Conjectures: OEIS A102371 identity

• 2026-08-15 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4970 with a kernel-checked Lean 4 proof answering the OPEN OEIS A102371 question affirmatively for every n≥1. Let R(n) be the finite bit-selected sum occurring in A105033 and define the sloping and carry parts by S(n)=n−R(n) and C(n)=R(n)+1. The proof establishes S(n)+C(n)=n+1, C(n+1)=2·(S(n) AND C(n))+1, and S(n+1)=S(n) XOR C(n); the last identity uses the binary full-adder relation (x XOR y)+2·(x AND y)=x+y. It then proves a fixed-width complement/XOR lemma and applies it inductively to the recurrence defining A102371. This yields a(n)=2^n−1−A105033(n−1), exactly the formula asked in the OEIS comment and registered in OeisA102371.conjecture. No additional generalization about either sequence is claimed. The fixed proof has no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4970kernel-checked Lean proof (fixed commit)carry and XOR proof developmentOEIS A102371OEIS A105033GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA102722.conjecture as research open with a theorem-body sorry; the submitted proof establishes the exact asymptotic-equivalence target without an extra error-bound hypothesis.
• 🔗 Source problem Formal Conjectures: OEIS A102722 asymptotic conjecture

Problem. Let $a(n)=\left\lfloor\sum_{k=1}^{n}\{n/k\}\right\rfloor$. Prove that $a(n)\sim(1-\gamma)n$, where $\gamma$ is the Euler–Mascheroni constant. — Formal Conjectures: OEIS A102722 asymptotic conjecture

• 2026-08-15 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4971 with a kernel-checked Lean 4 proof of the OPEN OEIS A102722 asymptotic conjecture, with no additional hypothesis. Write S(n)=∑_{k≤n}{n/k}, D(n)=∑_{k≤n}⌊n/k⌋, and r=⌊√n⌋. The proof first establishes the exact identity S(n)=nHₙ−D(n) and formalizes Dirichlet's hyperbola identity D(n)=2∑_{k≤r}⌊n/k⌋−r² by counting lattice points with product at most n. Bounding each floor error by 1 controls the truncated divisor sum within r of nHᵣ. Mathlib's harmonic-number limit together with r/n→0, r²/n→1, and 2 log r−log n→0 then gives D(n)/n−log n→2γ−1 and S(n)/n→1−γ. Finally, taking the outer floor changes the normalized value by at most 1/n, so a(n)/n→1−γ; since 1−γ≠0, this is converted to the exact asymptotic equivalence a(n)~(1−γ)n. The fixed proof has no sorry, admit, custom axiom, native_decide, or unsafe theorem; its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4971exact FC theorem (fixed commit)complete analytic proof (fixed commit)OEIS A102722GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks OeisA112521.conjecture as research open with a theorem-body sorry; the submitted proof establishes the exact target for every n≥1 without a bridge hypothesis.
• 🔗 Source problem Formal Conjectures: OEIS A112521 diagonal conjecture

Problem. Let $T(1,1)=1$, let $T(i,j)=0$ outside the positive quadrant, and define $T$ by the stated five-term recurrence. Prove that $a(n)=T(n,n)$ for every $n\ge1$. — Formal Conjectures: OEIS A112521 diagonal conjecture

• 2026-08-15 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #4972 with a complete, kernel-checked Lean 4 proof of the OPEN OEIS A112521 main-diagonal conjecture. Define S(d)=∑_{0≤j≤d}(−1)^j C(2j,j) C(2d−j,d−j). The proof constructs homogeneous Fibonacci polynomials and applies the linear change v=x+y, u=x−y; the transformed coefficients satisfy exactly the five-term recurrence defining T, which identifies T(d+1,d+1) with S(d). A fully formalized Wilf–Zeilberger telescoping certificate then proves, for n≥3, the recurrence 5n(n+1)S(n+1)=2n(2n+1)S(n)+4(16n²−1)S(n−1). Together with four explicit initial cases, its positive coefficients establish S(d)≥0. Rewriting the signed sum inside a(d+1) as S(d) and using nonnegativity to remove Int.toNat completes a(n)=T(n,n) for every n≥1. All WZ identities and boundary terms are proved in Lean; no unproved bridge assumption is used. The fixed proof has no sorry, admit, custom axiom, native_decide, or unsafe theorem, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #4972final kernel-checked theorem (fixed commit)complete coefficient and WZ proof (fixed commit)OEIS A112521GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks all four displayed divisibility declarations as research open, each with a theorem-body sorry. The separate general_divisibility declaration remains open and is vacuous as written because it permits D=0. Issue #4923 now records an explicit positive witness proposed for the intended repair; its paper proof is reported complete but has not yet been kernel-checked in Lean. The independent supercongruence target also remains open.
• 🔗 Source problem Formal Conjectures: four OEIS A211417 divisibility conjectures

Problem. For $a(n)=(30n)!n!/((15n)!(10n)!(6n)!)$, prove $(2n+1)\mid7a(n)$, $(3n+1)\mid a(n)$, and $(5n+1)\mid a(n)$; deduce $(2n+1)(3n+1)(5n+1)\mid42a(n)$. — Formal Conjectures: four OEIS A211417 divisibility conjectures

• 2026-08-16 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #5010 with kernel-checked Lean 4 proofs of four OPEN OEIS A211417 targets. For the three mathematically substantive atomic assertions, the proof expresses the p-adic valuation of the factorial ratio through the nonnegative Landau term F(n,m)=⌊30n/m⌋+⌊n/m⌋−⌊15n/m⌋−⌊10n/m⌋−⌊6n/m⌋ and sums its prime-power contributions using Legendre's formula. General residue lemmas cover all but finitely many exceptional prime powers; the exceptional 2-, 3-, 5-, and 7-primary parts are supplied by binomial-coefficient valuation identities and explicit higher-power Landau contributions. This proves (2n+1)∣7a(n), (3n+1)∣a(n), and (5n+1)∣a(n) for every natural n. The fourth FC target is then derived rather than counted as an independent discovery: gcd(2n+1,3n+1)=1, while the remaining pairwise overlaps divide 3 and 2, so the product divides 42a(n). The fixed proofs contain no sorry, admit, custom axiom, native_decide, or unsafe theorem for these four targets; their axiom audits report only propext, Classical.choice, and Quot.sound. The general divisibility declaration and the separate supercongruence are not claimed solved. A 2026-08-16 update to issue #4923 proposes the positive general witness D(r)=lcm(1,…,r)^|{1≤i≤r : gcd(i,30)=1}|; its proof is paper-complete but is explicitly not yet Lean-checked.
  Formal Conjectures PR #5010A211417 general-divisibility update — issue #4923four exact FC targets and axiom audit (fixed commit)complete proof development (fixed commit)OEIS A211417GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Conjecture 5 as research open with a theorem-body sorry. PR #5011 submits a complete proof and changes that declaration to research solved.
• 🔗 Source problem Formal Conjectures: arXiv 2607.03582 Conjecture 5

Problem. Let $K\subset\mathbb R^2$ be a compact convex body with a centre of symmetry, containing the origin. For $p>1$, equality in the sharp $L_p$ Rogers--Shephard volume bound implies that $K$ is a parallelogram with a vertex at the origin. — Formal Conjectures: arXiv 2607.03582 Conjecture 5

• 2026-08-16 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #5011 with a complete Lean 4 proof of the OPEN Conjecture 5 from Fradelizi–Manui–Meyer–Ndiaye (2026). The argument develops an endpoint–fiber rigidity theorem. A lower bound for each fiber of the Lₚ sum, together with the assumed equality of total volumes, layer-cake integration, and continuity, forces equality for every interior fiber. Choosing a support point orthogonal to the centre of symmetry then determines the exact fiber intervals along the relevant ray. Their endpoints trace four boundary segments; supporting functionals trap the centered body inside the quadrilateral generated by the symmetry centre and support point. After translation this identifies the original body as a parallelogram having the origin as a vertex. The fixed proof contains no sorry, admit, custom axiom, native_decide, or unsafe theorem, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The linked repository also contains a separate proof of Conjecture 4, but PR #5011 targets Conjecture 5, so this entry counts only the Conjecture 5 contribution.
  Formal Conjectures PR #5011exact FC theorem proof and axiom audit (fixed commit)complete proof development (fixed commit)source paper — arXiv:2607.03582GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks the 2-adic asymptotic as research open with a theorem-body sorry. PR #5013 submits its complete proof and changes only this declaration to research solved; the separate p≡1 (mod 4) valuation conjecture remains open.
• 🔗 Source problem Formal Conjectures: OEIS A105751 2-adic conjecture

Problem. For $a(n)=\operatorname{Im}\prod_{k=0}^n(1+ki)$, prove $\nu_2(a(n))\sim n/4$ as $n\to\infty$. — Formal Conjectures: OEIS A105751 2-adic conjecture

• 2026-08-16 formal conjectures lean proof submission
  Submitted Formal Conjectures PR #5013 with a kernel-checked Lean 4 proof of the OPEN 2-adic asymptotic for OEIS A105751. Writing the defining complex product as the image of a Gaussian-integer product gives an exact recurrence for its real and imaginary coordinates. The proof normalizes four-factor blocks, pairs adjacent blocks into even- and odd-start polynomial superblocks, and uses their parity and cross-difference divisibility in a dyadic induction. This yields exact formulas for every residue class: ν₂(a(4m+1))=m, ν₂(a(4m+2))=m, ν₂(a(4m))=m+2+ν₂(⌈m/2⌉), and ν₂(a(4m+3))=m+3+ν₂(⌈m/2⌉) away from the two zero terms. Consequently the error from n/4 is logarithmic; Lean proves the normalized error bound (12+4 log₂ n)/n, shows that it tends to zero, and applies the squeeze theorem to the exact Formal Conjectures target. The fixed theorem has no sorry, admit, custom axiom, native_decide, or unsafe dependency, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The separate conjecture for primes p≡1 (mod 4) is outside this proof and remains open.
  Formal Conjectures PR #5013exact FC theorem and axiom audit (fixed commit)complete proof development (fixed commit)OEIS A105751GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted asks for the next semiprime using answer(sorry) and marks the target research open. PR #5014 supplies its exact numerical answer and changes only next_semiprime to research solved; the separate question asking whether another prime occurs after a(2)=5 remains open.
• 🔗 Source problem Formal Conjectures: OEIS A100474 next-semiprime question

Problem. For the recursively defined sequence $a(n)$ in OEIS A100474, determine the first semiprime term occurring after $a(11)$. — Formal Conjectures: OEIS A100474 next-semiprime question

• 2026-08-16 formal conjectures exact-answer submission
  Submitted Formal Conjectures PR #5014 with the exact answer to the OPEN A100474 next-semiprime question: the first qualifying term after a(11) is a(36), a 133-digit integer factoring as 251 × p, where p is a 131-digit prime. The Lean development certifies the first 665 primes, evaluates the defining recurrence sequentially through index 36, and excludes every index from 12 through 35 using explicit three-factor decompositions. It proves the large cofactor prime with a recursive Lucas certificate and kernel-checked square-and-multiply modular traces, then establishes that 36 is the least qualifying index and rewrites the exact sInf target. The proof uses neither native_decide nor compiler-trusted evaluation; the final theorem has no sorryAx, Lean.trustCompiler, or Lean.ofReduceBool, and its axiom audit reports only propext, Classical.choice, and Quot.sound. This is a complete certified answer to the semiprime question, not a solution of the separate prime-occurrence conjecture, which remains open.
  Formal Conjectures PR #5014exact FC theorem and axiom audit (fixed commit)complete proof development (fixed commit)OEIS A100474GitHubLean4Web

• 🔵 Status when posted SOLVED — Formal Conjectures source when submitted already marks the k=3 variant research solved, crediting an unpublished result of Erdős, while the all-k statement remains research open. PR #5017 adds the new independent kernel-checked proof as its formal_proof; this entry is therefore not counted as a newly solved open problem.
• 🔗 Source problem Formal Conjectures: Erdős #979 k=3 variant

Problem. If $f_3(n)$ counts representations of $n$ as a sum of three prime cubes, prove $\limsup_{n\to\infty} f_3(n)=\infty$. — Formal Conjectures: Erdős #979 k=3 variant

• 2026-08-17 independent lean proof registration
  Submitted Formal Conjectures PR #5017 to register a complete Lean 4 proof of the exact k=3 variant of Erdős Problem 979: the limsup of the number of representations of an integer as a sum of three prime cubes is infinite. Formal Conjectures already classified this variant as solved on the strength of an unpublished assertion by Erdős, but no text of his proof is publicly cited; the submitted development is an independent proof, not a reconstruction of the unpublished argument. It follows a modern complex-multiplication route. Point counts for the Fermat cubic are controlled through cubic Jacobi sums; primary Eisenstein integers encode the relevant Hecke angles; lattice-point and thin-annulus estimates produce Dirichlet-series models; and Wiener–Ikehara together with the prime number theorem in the progression 1 modulo 3 yields an unbounded supply of suitable prime triples. An injection from sorted triples to multisets then proves the literal Formal Conjectures target. The modular development spans 52 project modules, and the standalone Lean4Web file is about 25,700 lines. The final axiom audit reports only propext, Classical.choice, and Quot.sound, with no sorryAx. The proof does not settle the all-k form of Problem 979 or give a quantitative growth rate for f₃.
  Formal Conjectures PR #5017exact FC theorem and axiom audit (fixed commit)proof repository README (fixed commit)Erdős Problem 979GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when reported marks the all-natural-n declaration research open, but issue #5022 gives a complete Lean disproof of its literal n=0 instance. The suggested repair is to require 0 < n, or 2 ≤ n in line with the neighboring conjecture; the intended positive-n problem remains open.
• 🔗 Source problem Formal Conjectures: VCDimConvex universal bound

Problem. The declaration quantifies over every $n\in\mathbb N$: for each $n$, is there a finite $d$ bounding the additive $\mathrm{VC}_n$ dimension of every convex set in $\mathbb R^{n+1}$? What happens at $n=0$? — Formal Conjectures: VCDimConvex universal bound

• 2026-08-18 formal conjectures misformalization report with lean disproof
  Opened Formal Conjectures issue #5022, labeled misformalization, to show that exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one is false because it quantifies over all natural numbers including zero. For an arbitrary proposed bound d, the Lean proof chooses the convex singleton C={0} in Fin 1 → ℝ. Since Fin 0 → Fin (d+1) has only one function, the degenerate zero-parameter setup allows translations of that singleton to realize every required membership pattern; hence HasAddVCNDimAtMost C 0 d fails for every d. The counterexample compiles against Formal Conjectures commit 9943b0a on Lean 4.27.0, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The issue proposes adding 0<n, or the stronger 2≤n used by the adjacent upper-bound conjecture. This is a precise disproof of the registered statement, not a solution of the intended positive-dimensional convex VCₙ problem, and it is independent of PR #4657's n=2, d=1 counterexample.
  Formal Conjectures issue #5022 and Lean disproofFormal Conjectures source (fixed commit)self-contained Lean4Web disproofrelated n=2, d=1 counterexample — PR #4657introducing PR #1408

• 🟢 Status when posted OPEN — Formal Conjectures PR source when proved marks all four A129365 targets research open with theorem-body sorrys. The pinned external development proves their exact headers. PR #5016 itself remains open, so these declarations are not yet on Formal Conjectures main; the OEIS entry also still labels A–D as conjectures as of 2026-08-18.
• 🔗 Source problem Formal Conjectures PR #5016: OEIS A129365 targets

Problem. For the ratio $a(n)$ of the double GCD product to $\prod_{k=1}^n\lfloor n/k\rfloor!^k$, prove its integrality; characterize its prime divisors by $p\le\lfloor n/3\rfloor$; prove that $\operatorname{ord}_p a(np+k)$ is constant for $0\le k<p$; and express that valuation as $\sum_{i\ge0}b(\lfloor n/p^i\rfloor)$ for OEIS A004125's remainder sum $b$. — Formal Conjectures PR #5016: OEIS A129365 targets

• 2026-08-18 formal conjectures lean proof publication
  Published kernel-checked Lean 4 proofs of all four research open OEIS A129365 targets introduced in Formal Conjectures PR #5016. The proof establishes the master identity vₚ(a(N)) = Σ_{r≥1} b(⌊N/pʳ⌋), where b(m)=Σ_{k=1}^m(m mod k) is OEIS A004125. At each prime-power level, the numerator's double GCD product contributes m², because exactly m=⌊N/pʳ⌋ indices are divisible by pʳ. Legendre's factorial formula turns the denominator contribution into Σ_{k=1}^m k⌊m/k⌋; subtracting and using division with remainder gives m²-Σ k⌊m/k⌋=Σ(m mod k)=b(m). Nonnegativity of this sum proves that the denominator divides the numerator. Since b(m)>0 exactly when m≥3, a prime divides a(n) exactly when p≤⌊n/3⌋. The floor quotients are unchanged throughout each block np,…,np+p-1, proving valuation invariance, and substituting N=np with an index shift gives the exact infinite-sum formula, whose support is finite. Both the Formal Conjectures and standalone Mathlib builds use Lean 4.27.0; the four axiom audits report only propext, Classical.choice, and Quot.sound, with no sorryAx, custom axiom, native_decide, or unsafe theorem. This entry counts as one solved problem family and four proved target statements.
  Formal Conjectures proof report in PR #5016four exact proofs and axiom audits (fixed commit)proof explanation and status boundary (fixed commit)OEIS A129365OEIS A004125Formal Conjectures PR #5016GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures PR source when proved marks the exact target research open with a theorem-body sorry. The equivalence is nevertheless classical and was already recorded on OEIS A003625 in 2018; the contribution is a proof/status sync and kernel-checked formalization, not a new mathematical solution. PR #5016 remains open.
• 🔗 Source problem Formal Conjectures PR #5016: OEIS A003625 target

Problem. For every prime $p$, prove that $p\equiv3,5,$ or $6\pmod 7$ if and only if $x^2+x+2$ is irreducible over $\operatorname{GF}(p)$. — Formal Conjectures PR #5016: OEIS A003625 target

• 2026-08-19 formal conjectures lean proof publication
  Published a kernel-checked Lean 4 proof of the exact research open OEIS A003625 target introduced in Formal Conjectures PR #5016. Completing the square gives 4(x²+x+2)=(2x+1)²+7, so for odd primes away from 7, reducibility is equivalent to −7 being a quadratic residue. Quadratic reciprocity and the first supplement cancel their signs to identify the Legendre symbols (−7/p)=(p/7). The nonresidues modulo 7 are precisely 3, 5, and 6, while the exceptional primes 2 and 7 are checked directly and make both sides false. The Formal Conjectures and standalone Mathlib versions both build with Lean 4.27.0; the final axiom audit reports only propext, Classical.choice, and Quot.sound, with no sorryAx, custom axiom, native_decide, or unsafe theorem. Because the equivalence was already stated on OEIS by Federico Provvedi in 2018 and is a classical quadratic-reciprocity consequence, this record carries the Literature tag and is excluded from counts of newly solved open mathematical problems.
  Formal Conjectures proof report in PR #5016exact proof and axiom audit (fixed commit)proof explanation and status boundary (fixed commit)OEIS A003625Formal Conjectures PR #5016GitHubLean4Web

• 🔵 Status when posted SOLVED — Affected Formal Conjectures declaration marks lower_bound research solved, but reverses the two sides of ≫ and therefore states an upper bound instead. The adjacent Erdős–Hall conjecture remains research open; issue #5062 proposes only a statement correction, not a solution of that conjecture.
• 🔗 Source problem Formal Conjectures: reversed Erdős #394 lower_bound

Problem. The docstring records the known lower bound $\sum_{n\le x}t_2(n)\gg x^2/\log x$. Does the Lean declaration encode that direction, while leaving the Erdős–Hall upper-bound conjecture open? — Formal Conjectures: reversed Erdős #394 lower_bound

• 2026-08-19 formal conjectures misformalization report
  Opened Formal Conjectures issue #5062, labeled misformalization, after detecting that erdos_394.variants.lower_bound reverses the two sides of the project's ≫ notation. The docstring correctly says Σ_{n≤x}t₂(n) ≫ x²/log x, a trivial known lower bound coming from t₂(p)=p−1 on primes. But since f≫g is defined as g=O(f), the code instead says Σt₂(n)=O(x²/log x), an upper bound. That accidental upper bound is far stronger: because log 2<1, it would imply the file's research open Erdős–Hall statement Σt₂(n)=o(x²/(log x)^c) for every c<log 2, allowing the open conjecture to be closed without new mathematics. The proposed fix simply swaps the arguments of ≫; the corrected lower bound stays research solved, while hall_conjecture meaningfully remains open. No other declaration is affected. This is a statement-direction correction, not a proof of Erdős Problem 394 or the Erdős–Hall conjecture.
  Formal Conjectures misformalization issue #5062affected declaration (fixed commit)definition of ≫ in Formal ConjecturesErdős Problem 394related status-sync issue #4803

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the universal exact-divisibility assertion research open, while OEIS A078590 still asks whether all terms are integers. PR #5078 supplies the negative answer and changes the declaration to research solved; the PR remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A078590 integrality target

Problem. Starting with $a(1)=a(2)=1$ and $a(n)=(2^{a(n-1)}+1)/a(n-2)$, are all terms integers? — Formal Conjectures: open OEIS A078590 integrality target

• 2026-08-21 formal conjectures counterexample submission
  Published a kernel-checked Lean 4 counterexample to the open integrality question for OEIS A078590 and submitted it in Formal Conjectures PR #5078. The first six recurrence terms are integers, with a(5)=171. Rather than expanding the enormous value 2^a(6), the proof computes a(6)≡3 (mod 18) and uses 2^18≡1 (mod 171) to obtain 2^a(6)+1≡9 (mod 171). Thus 171 does not divide the seventh numerator, so the exact Formal Conjectures universal-divisibility target is false at n=7; moreover the gcd is 9, making the seventh rational term's reduced denominator 171/9=19. The PR replaces the false positive proposition by the yes/no statement with answer(False) and marks it research solved. The Formal Conjectures and standalone Mathlib versions use Lean 4.27.0. The axiom audit reports only propext, Classical.choice, and Quot.sound, with no sorryAx, custom axiom, native_decide, or unsafe theorem. This is a complete negative answer to the OEIS question, not merely a formalization of a previously known result.
  Formal Conjectures PR #5078exact counterexample and negative-answer proof (fixed commit)proof explanation and status boundary (fixed commit)OEIS A078590Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the combined divisibility-and-squarefree assertion research open, while OEIS A070823 still presents the squarefree-cofactor claim as a question. PR #5079 supplies the negative answer and changes the single declaration to research solved; the PR remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A070823 squarefree target

Problem. For the recurrence formed by the absolute difference of the two decimal concatenations of consecutive terms, is every $a(n)$ with $n>2$ divisible by $3$ and expressible as $2^j3^k s$ with $s$ squarefree? — Formal Conjectures: open OEIS A070823 squarefree target

• 2026-08-21 formal conjectures counterexample submission
  Published a kernel-checked Lean 4 counterexample to the open squarefree-cofactor question for OEIS A070823 and submitted it in Formal Conjectures PR #5079. The proof also settles the statement's first conjunct positively: because 10≡1 (mod 3), concatenating x,y or y,x gives the same residue x+y, so their absolute difference is divisible by 3 for every n>2. The second conjunct fails at n=20. Kernel reduction gives the compact certificate a(20) mod 13³ = 1859 = 13²·11, hence 13²∣a(20). Since 13 is coprime to every factor 2^j3^k, any decomposition a(20)=2^j3^k s forces 13²∣s, contradicting the requirement that s be squarefree. The PR keeps the existing single target, replaces its false universal positive form by answer(False), and marks it research solved. The Formal Conjectures and standalone Mathlib versions use Lean 4.27.0, contain no sorry, admit, custom axiom, native_decide, or unsafe theorem, and include explicit axiom audits. This is a complete negative answer to the OEIS question, not merely a formalization of a previously known result.
  Formal Conjectures PR #5079divisibility proof, counterexample, and axiom audits (fixed commit)proof explanation and status boundary (fixed commit)OEIS A070823Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks Conjecture 1 research open, matching OEIS A159829's unresolved question for exponents above 2. PR #5081 supplies the negative answer and changes only Conjecture 1 to research solved; Conjecture 2 about n^k+m^k+1 remains open and unchanged. PR #5081 remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A159829 Conjecture 1

Problem. For every integer $k\ge3$, are there infinitely many primes of the form $n^k+m^k$ with $n,m\ge1$? — Formal Conjectures: open OEIS A159829 Conjecture 1

• 2026-08-21 formal conjectures counterexample submission
  Published a kernel-checked Lean 4 negative answer to OEIS A159829 Conjecture 1 and submitted it in Formal Conjectures PR #5081. The proof establishes the stronger theorem that for every odd k≥3, the set of prime values n^k+m^k with positive n,m is exactly the singleton {2}. Oddness gives the factorization n+m ∣ n^k+m^k. If the sum is prime, the nontrivial divisor n+m must equal the entire sum; but as soon as either input exceeds 1, the inequality n+m<n^k+m^k contradicts that equality. Hence n=m=1 and the value is 2. Specializing to k=3 makes the prime-value set finite and refutes the original universal infinitude assertion. The PR replaces Conjecture 1 by the explicit negative answer answer(False) and marks it research solved, while leaving the separate n^k+m^k+1 Conjecture 2 unchanged and open. The Formal Conjectures and standalone Mathlib versions use Lean 4.27.0; the axiom audits report only propext, Classical.choice, and Quot.sound, with no sorryAx, custom axiom, native_decide, or unsafe theorem. This is a complete negative answer to Conjecture 1, not a claim about the unresolved even-exponent cases or Conjecture 2.
  Formal Conjectures PR #5081odd-exponent classification, counterexample, and axiom audits (fixed commit)proof explanation and scope boundary (fixed commit)OEIS A159829Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks Peter Bala's Gauss-congruence Conjecture 3 research open, as does the current OEIS A185895 entry. PR #5083 supplies a proof and changes only Conjecture 3 to research solved; the separate sign-change Conjectures 1 and 2 remain open. PR #5083 remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A185895 Conjecture 3

Problem. For the coefficients $a(N)=N![x^N]\prod_{j\ge1}(1-x^j/j!)$, prove for every prime $p$ and positive $n,k$ that $a(np^k)\equiv a(np^{k-1})\pmod{p^k}$. — Formal Conjectures: open OEIS A185895 Conjecture 3

• 2026-08-21 formal conjectures lean proof submission
  Published a kernel-checked Lean 4 proof of OEIS A185895 Conjecture 3 and submitted it in Formal Conjectures PR #5083. Expanding the defining product and eliminating the rational coefficient followed by floor rewrites a(N) as a signed sum over sets of distinct positive block sizes whose sum is N; each summand is the associated multinomial coefficient. The proof then works coefficientwise in a multivariate polynomial ring over ZMod(p^k). A prime-power freshman's-dream argument shows that, at total degree p·m, a multinomial coefficient vanishes modulo p^k unless every multiplicity is divisible by p; in the surviving case it reduces to the coefficient with all multiplicities divided by p. The surviving finite sets are reindexed by the bijection s↔p·s, which preserves cardinality and therefore the sign. Taking m=n·p^(k−1) yields a(np^k)≡a(np^(k−1)) (mod p^k) for every prime p and positive n,k. The proof uses the general Gauss/Dold mechanism as mathematical background but establishes the exact OEIS target directly. The Formal Conjectures and standalone Mathlib versions use Lean 4.27.0; the final axiom audit reports only propext, Classical.choice, and Quot.sound, with no sorryAx or custom axiom. Conjectures 1 and 2 concern separate sign-change phenomena and are explicitly left open.
  Formal Conjectures PR #5083exact Gauss-congruence theorem and axiom audit (fixed commit)proof architecture and scope boundary (fixed commit)OEIS A185895Formal Conjectures source before submission (fixed commit)Gossow — polynomial and combinatorial analogues of Gauss congruenceGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the alternating recurrence theorem research open; OEIS A022030 likewise still lists the recurrence as a conjecture. PR #5085 supplies a proof and changes the target to research solved. The older non-alternating sequence mentioned in the OEIS comments is a different problem and is not counted here. PR #5085 remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A022030 recurrence target

Problem. For the alternating sequence beginning $4,16,63,249,984,\ldots$, prove that for every $n\ge4$, $a(n)=4a(n-1)-a(n-3)+a(n-4)$. — Formal Conjectures: open OEIS A022030 recurrence target

• 2026-08-21 formal conjectures lean proof submission
  Published a kernel-checked Lean 4 proof of the exact open Formal Conjectures target for OEIS A022030 and submitted it in PR #5085. The proof carefully targets the current alternating definition, whose terms begin 4,16,63,249,984,…: even steps use ceiling minus one and odd steps use floor plus one. It introduces the linear candidate L with the claimed recurrence and proves positivity plus the growth bound 3Lₙ≤Lₙ₊₁. A signed determinant defect Eₙ=(-1)ⁿ(Lₙ₊₁²−LₙLₙ₊₂) satisfies a positive-coefficient order-ten recurrence; checking its initial values and propagating the bounds 0<Eₙ≤Lₙ show that the nonlinear ceiling/floor step is exactly Lₙ₊₂ at every index. Therefore the original sequence equals L, giving a(n)=4a(n−1)−a(n−3)+a(n−4) for all n≥4. This is the alternating Formal Conjectures target, not the older non-alternating sequence also discussed in OEIS comments. The proof repository uses Lean 4.27.0, has no sorry, admit, custom axiom, native_decide, or unsafe declaration, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #5085exact recurrence proof and axiom audit (fixed commit)proof explanation and alternating-sequence scope (fixed commit)OEIS A022030Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the combined ζ(3)-tail and Beatty-difference proposition research open; the current OEIS A049473 entry likewise presents it as a conjecture. PR #5087 proves both conjuncts while leaving the statement unchanged, and changes the target to research solved. PR #5087 remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A049473 target

Problem. For the nearest-integer sequence $a(n)=\operatorname{round}(n/\sqrt2)$ and $s(m)=\zeta(3)-\sum_{k=1}^m k^{-3}$, prove both $s(a(n))<1/n^2<s(a(n)-1)$ and the A001954/A001953 classification of the zero/one positions of $a(n)-a(n-1)$. — Formal Conjectures: open OEIS A049473 target

• 2026-08-21 formal conjectures lean proof submission
  Published a kernel-checked Lean 4 proof of the full open Formal Conjectures target for OEIS A049473 and submitted it in PR #5087. For the nearest-integer sequence a(n)=⌊n/√2+1/2⌋, the proof first establishes two telescoping bounds for the ζ(3) tail s(m)=ζ(3)−Σₖ₌₁ᵐ1/k³: an upper bound below 1/(2m(m+1)) and a lower bound above 1/(2m²−2m+1). The nearest-integer inequalities yield the matching quadratic bounds 2m²−2m+1≤n²≤2m(m+1), which combine to give s(a(n))<1/n²<s(a(n)−1). The proof then derives the difference classification from exact floor inequalities and irrationality of √2: one-steps occur at the A001953 Beatty positions and zero-steps at the complementary A001954 positions. Thus both conjuncts of the original theorem are proved, not just the more elementary Beatty component. The repository uses Lean 4.27.0; its proof files contain no sorry, admit, custom axiom, native_decide, or unsafe declaration, and the axiom audits report only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #5087exact target proof and axiom audits (fixed commit)proof explanation and two-conjunct scope (fixed commit)OEIS A049473Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the question whether a(n)≤1 for all n as research open; OEIS A076141 likewise poses this as a question. PR #5088 supplies a proof and changes the target to research solved. PR #5088 remains open as of 2026-08-21.
• 🔗 Source problem Formal Conjectures: open OEIS A076141 target

Problem. Let $a(n)$ count the (possibly overlapping) occurrences of the most-significant-bit-first binary word of $n$ in the binary word of $n^2$. Prove that $a(n)\le1$ for every $n\in\mathbb{N}$. — Formal Conjectures: open OEIS A076141 target

• 2026-08-21 formal conjectures lean proof submission
  Published a kernel-checked Lean 4 proof of the exact open Formal Conjectures target for OEIS A076141 and submitted it in PR #5088. The imported definition counts every occurrence, including overlaps, of the most-significant-bit-first binary word of n in the binary word of n². Assuming two distinct starts, the proof converts the two list-prefix matches into arithmetic block equations for n²; their overlap gives a period for the binary word of n. Careful lower and upper block decompositions, together with the needed power-of-two and coprimality bounds, then split into the possible signs of an auxiliary integer and force an impossible negative or oversized remainder. Hence two distinct occurrences cannot exist, while the n=0 case is discharged directly from the exact list definition. The proof uses the literal Formal Conjectures definitions rather than a surrogate theorem. The repository uses Lean 4.27.0; its proof files contain no sorry, admit, custom axiom, native_decide, or unsafe declaration, and the axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #5088exact uniqueness theorem and axiom audit (fixed commit)proof explanation and exact-definition scope (fixed commit)OEIS A076141Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source immediately before submission marks the literal universal-ε higher-full-parts question research open; the Erdős Problems page uses the same universal wording. PR #5090 proves that this literal statement is false and changes only this variant to research solved. The main declaration erdos_367.parts.i, Erdős Problem 367 overall, and the mathematically meaningful corrected variant with ∃ ε>0 all remain open. PR #5090 remains open as of 2026-08-22.
• 🔗 Source problem Formal Conjectures: open literal higher-full-parts variant

Problem. For every $r\ge3$, $k\ge2$, and $\varepsilon>0$, must $\limsup_{n\to\infty}\prod_{n\le m<n+k}B_r(m)/n^{1+\varepsilon}=\infty$, where $B_r(m)$ is the $r$-full part of $m$? — Formal Conjectures: open literal higher-full-parts variant

• 2026-08-22 formal conjectures literal-target disproof submission
  Published a kernel-checked Lean 4 disproof of the literal open Formal Conjectures higher-full-parts variant attached to Erdős Problem 367 and submitted it in PR #5090. The target quantifies over every positive ε; specializing to (r,k,ε)=(3,2,2) already gives a counterexample. From the definition of the r-full part, the proof establishes B r m ∣ m, hence B₃(n)B₃(n+1)≤n(n+1). After division by n^(1+2)=n³, the resulting EReal-valued sequence is eventually bounded by the finite value 2, so its limsup cannot be ⊤. This proves the exact imported target with answer(False). The scope boundary is essential: the result detects the flaw in the literal ∀ ε>0 formulation; it does not solve erdos_367.parts.i, Erdős Problem 367 as a whole, or the corrected question asking whether a suitable ε>0 exists. The proof uses Lean 4.27.0, contains no sorry, admit, custom axiom, native_decide, or unsafe declaration, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures PR #5090exact disproof and axiom audit (fixed commit)proof explanation and scope boundary (fixed commit)Erdős Problem 367Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 🟢 Status when posted OPEN — archived Open Problem Garden problem page presents Melnikov's strict chromatic lower bound as an unanswered problem. Formal Conjectures did not yet contain this target; issue #5092 proposes adding it directly as research solved with answer(False) and links the completed Lean proof. The issue is open and marked up for grabs as of 2026-08-22, so this records a solution of the external problem and an addition proposal, not an upstream Formal Conjectures merge.
• 🔗 Source problem Open Problem Garden: Melnikov's valency-variety problem (archived)

Problem. For every finite simple graph $G$ with at least two vertices, is $\chi(G)>\left\lceil\lfloor w(G)/2\rfloor/(|V(G)|-w(G))\right\rceil$, where $w(G)$ is the number of distinct vertex degrees? — Open Problem Garden: Melnikov's valency-variety problem (archived)

• 2026-08-22 open problem garden counterexample and formal conjectures addition proposal
  Published a kernel-checked Lean 4 counterexample to Melnikov's valency-variety problem and opened Formal Conjectures issue #5092 proposing that the problem be added as an already solved answer(False) entry. The explicit graph has 37 vertices partitioned into independent sets of sizes 6, 10, and 21. Its degree set is exactly {0,…,29}, so w(G)=30; the displayed tripartition gives a 3-colouring, while an explicit triangle forces chromatic number at least 3, hence χ(G)=3. Melnikov's proposed bound evaluates to ceil(floor(30/2)/(37−30))=ceil(15/7)=3, so the universal strict inequality fails by equality. The graph is disconnected and contains one isolated vertex, which is sufficient for the problem exactly as stated because no connectedness hypothesis is imposed; the proof does not claim a connected counterexample or determine the optimal replacement bound. The prospective Formal Conjectures-style statement is explicitly unofficial because no target was registered upstream when the issue was opened. The proof uses Lean 4.27.0, contains no sorry, admit, custom axiom, native_decide, or unsafe declaration, and its axiom audit reports only propext, Classical.choice, and Quot.sound.
  Formal Conjectures issue #5092prospective FC statement (unofficial, fixed commit)exact counterexample theorem and axiom audit (fixed commit)construction, proof explanation, and scope (fixed commit)archived Open Problem Garden problemGitHubLean4Web

• 🟢 Status when posted OPEN — Formal Conjectures source when submitted marks Green29.green_29 research open with an unknown Boolean answer. A public validator result had already accepted, kernel-verified, and review-approved a counterexample to this exact pinned target on 2026-08-06. PR #5094 adapts and packages that public proof for the Formal Conjectures import and proposes answer(False). The already-solved weaker declaration Green29.green_29.variant, which drops S ⊆ A and allows the density constant to depend on K, is separate and unchanged. PR #5094 remains open as of 2026-08-22.
• 🔗 Source problem Formal Conjectures: open Green Problem 29 target

Problem. Do there exist absolute constants $C,c>0$ such that every $K$-approximate group $A$ contains $S\subseteq A$ with $|S|\ge C K^{-c}|A|$ and $S^8\subseteq A^4$? — Formal Conjectures: open Green Problem 29 target

• 2026-08-22 formal conjectures proof adaptation and solved-status submission
  Prepared an FC-facing Lean 4 repository and submitted Formal Conjectures PR #5094 to change the exact OPEN target Green29.green_29 from answer(sorry) to answer(False). The mathematical proof is explicitly adapted from public validator submission 82ab85ee-5dfc-4775-b3e1-8abc16e213b9, credited there to hotkey 5GeGrYFpMrNSh3Nwcx987zWz4cME9A9NbCkEbjBvv4uLUScV; it was accepted, kernel-verified, and review-approved on 2026-08-06. Thus this record credits the contribution as a proof adaptation and upstream status correction, not as an independent discovery of the counterexample. The construction takes an arbitrarily large finite group H and the slab A=({−1}×H)∪({1}×H)∪{(0,1)} inside Multiplicative ℤ×H. Three translates cover A², so A is a 3-approximate group and |A| grows with |H|. If S⊆A and S⁸⊆A⁴, comparing integer coordinates forces every element of S into the sole zero-layer point, hence |S|≤1. This contradicts every proposed positive lower density C·3^(−c) once H is large enough. The fixed proof establishes the exact imported proposition, contains no sorry, admit, custom axiom, native_decide, or unsafe declaration, and its axiom audit reports only propext, Classical.choice, and Quot.sound. The known weaker green_29.variant is not used as a substitute and remains unchanged.
  Formal Conjectures PR #5094FC-facing proof and axiom audit (fixed commit)proof provenance and mathematical explanation (fixed commit)public certified validator resultpublic validator solutionvalidator review decisionGreen's Open Problems, Problem 29Formal Conjectures source before submission (fixed commit)GitHubLean4Web

• 📨 Submission (2026-08-04) Kenta Kitamura changed the conjecture to a theorem and supplied a proof
• 📖 Published proof the current A059304 entry includes the proof under Kenta Kitamura’s name
• ✅ OEIS approval (2026-08-08) Sean A. Irvine changed the status from editing to approved

Theorem. For every $n\ge 0$, $a(n)=\sum_{0\le j,k\le n}\binom{n}{j}\binom{n}{k}\binom{j+k}{n}$, where $a(n)=2^n\binom{2n}{n}$. — A059304

• 2026-08-04 OEIS proof submission
  Submitted a proof of Peter Bala's conjectured identity for OEIS A059304. Using coefficient extraction, $\binom{j+k}{n}=[x^n](1+x)^{j+k}$, so the double sum is $[x^n](\sum_{j=0}^n\binom{n}{j}(1+x)^j)^2=[x^n](2+x)^{2n}=2^n\binom{2n}{n}=a(n)$. The published entry now labels the identity a theorem and includes this proof under Kenta Kitamura's name. OEIS editor Michel Marcus revised and reproposed the submission on 2026-08-04; Sean A. Irvine approved it on 2026-08-08.
  published OEIS entryKenta Kitamura submission (revision #118)Sean A. Irvine approval (revision #124)revision history

• 📨 Submission (2026-08-06) Lean-Eval issue #957
• 🥇 First accepted solution officially listed under “Newly-solved problems”; attempted 1 / 1, succeeded 1
• 🔒 Evaluated artifact immutable commit 5bef8d1

Benchmark. For every $n \ge 3$ and basepoint $x \in S^n$, the multiplicative group $\pi_{n+1}(S^n,x)$ is equivalent to $\mathbb{Z}/2$.

• 2026-08-06 Lean-Eval submission
  Produced the first complete Lean formalization accepted by Lean-Eval for this benchmark, proving it uniformly for all $n \ge 3$. Lean-Eval's official result records it under Newly-solved problems, establishing it as the first accepted solution for this benchmark within Lean-Eval. The proof follows Pontryagin's framed-cobordism route, without using a Hopf map or degree theory. The evaluated artifact comprises 448 submission modules and builds 9101 jobs; it uses only propext, Classical.choice, and Quot.sound, with no sorry, admit, native_decide, or bv_decide. The evaluation attempted 1 benchmark and succeeded on 1.
  Lean-Eval submission #957official resultimmutable evaluated artifactmaintained repository

• 📨 Submission (2026-08-03) Lean-Eval issue #911
• 🥇 First accepted solution officially listed under “Newly-solved problems”; attempted 1 / 1, succeeded 1
• 🔒 Evaluated artifact immutable commit f4e380b

Benchmark. A positive-definite quadratic form defined by an integral symmetric matrix is universal if and only if it represents every integer from $1$ through $15$.

• 2026-08-03 Lean-Eval submission
  Produced the first complete Lean formalization accepted by Lean-Eval for this benchmark. Lean-Eval's official result records conway_schneeberger_fifteen under Newly-solved problems, establishing it as the first accepted solution for the benchmark within Lean-Eval. The development formalizes the Conway–Schneeberger fifteen theorem via Bhargava's escalator-tree argument, including the supporting quadratic-form and number-theory machinery not previously available in Mathlib. The accepted artifact is a complete, sorry-free Lean 4 proof; it uses only propext, Classical.choice, and Quot.sound, with no native_decide or declared axioms. The evaluation attempted 1 benchmark and succeeded on 1.
  Lean-Eval submission #911official resultimmutable evaluated artifactmaintained repository

• 🔗 Invitation (2026-08-05) mo271 invited KitaKen1 to review the formalization
• 🔗 Review (2026-08-07) KitaKen1 posted the scoped technical review
• 🔗 Author response the author credited the review and revised the pull request
• ℹ️ Scope Definitions and parts (i)–(iii); explicitly excluded the [Ly26] certificates and the two claimed exact values.

At the invitation of Formal Conjectures collaborator mo271, reviewed arex1337's PR #4693, “feat(Erdős 176): formalize discrepancy progression numbers and exact values”. The review was explicitly scoped to the definitions and formalization of parts (i)–(iii), not the [Ly26] certificates or the claimed exact values. It confirmed the arithmetic-progression encoding looked faithful to the source and raised four non-blocking issues: the undocumented $2 \le k$ hypothesis, the missing explanation that threshold monotonicity covers $N \le 156$, the rationale for choosing $k=13,15$, and the inaccessible 5.17-GiB certificate archive. The author credited the careful review and revised the documentation, references, and archive packaging in response.

• 🔗 Forum report (10:32) reported the refutation of the remaining forward implication
• ℹ️ Scope Status and source curation of OpenAI's result; not authorship of the proof.

Posted a deliberately scoped update on Erdős #113: the problem had already been marked disproved via Janzer's counterexample to the reverse implication, while OpenAI's Chapter 10 result refutes the remaining forward implication. The entry does not present this as the first disproof of the whole problem.

• 🔗 Forum report (09:26) reported the Lean-verified counterexample to the degeneracy conjecture
• 🔗 Formal Conjectures issue #382 recommended treating Erdős #146 as a solved-result formalization target
• 🔗 Subsequent outcome (2026-08-07) PR #4715 added Erdős #146 as research solved
• ℹ️ Scope Status, source, and formalization-target curation of OpenAI's result; not authorship of the proof or of the later Formal Conjectures pull request.

Posted a source-backed update that OpenAI had resolved Erdős #146 by counterexample. The report identifies TwoDegenerateGraphs.not_erdos_146, links the official announcement and paper, and pins the Lean certificate to immutable commit a13547c. Also updated Formal Conjectures issue #382 with the theorem and recommended treating it as a solved-result formalization target. Williamjblair later added #146 as research solved in PR #4715.

• 🔗 Forum report (09:48) reported the formal negation of the compactness-conjecture statement
• 🔗 Formal Conjectures issue #407 recommended treating Erdős #180 as a solved-result formalization target
• 🔗 Subsequent outcome (2026-08-07) PR #4715 added Erdős #180 as research solved
• ℹ️ Scope Status, source, and formalization-target curation of OpenAI's result; not authorship of the proof or of the later Formal Conjectures pull request.

Posted a source-backed update that OpenAI had announced Erdős #180 as resolved. The report identifies CompactnessConjecture.not_erdos_180, which proves the direct negation of the formal conjecture statement, and links the immutable Lean certificate. Also updated Formal Conjectures issue #407 and recommended treating it as a solved-result formalization target. Williamjblair later added #180 as research solved in PR #4715.

• 🔗 Issue #409 report identified the Ramsey-number divergence theorem as a solved-result target
• 🔗 Subsequent outcome (2026-08-07) PR #4715 added Erdős #183 as research solved
• ℹ️ Scope Formalization-target curation of a third-party result; not authorship of either proof PR.

Reported in Formal Conjectures issue #409 that OpenAI had resolved Erdős #183. The comment identifies ErdosProblems.MulticolourTriangleRamsey.erdos_183, states that it proves R(3;k)^(1/k) → ∞, and recommends a solved-result formalization target. Williamjblair later added the result as research solved in merged PR #4715.

• 🔗 Forum report (10:17) reported the disproof of the corrected compactness conjecture
• 🔗 Formal Conjectures issue #804 linked the corrected compactness-conjecture disproof and immutable Lean source
• ℹ️ Scope Status, source, and formalization-target curation of OpenAI's result; not authorship of the proof.

Posted a source-backed update that Chapter 10 of OpenAI's paper disproves the corrected Erdős–Simonovits compactness conjecture and explicitly cites Erdős #575. The report also links the accompanying Lean formalization at immutable commit a13547c. Also updated Formal Conjectures issue #804 with the disproof and immutable Lean source.

• 🔗 Formal Conjectures issue #4680 requested an Ehrhart volume result entry categorized as research solved
• ℹ️ Scope Conjecture-database curation; the underlying mathematical and Lean proof is OpenAI's.

Opened Formal Conjectures issue #4680 to propose the Ehrhart volume result from OpenAI's ten-proofs release for inclusion as @[category research solved]. The proposal links the official article and paper, the immutable full Lean proof, and its compact Comparator Challenges statement template.

• 🔗 Formal Conjectures issue #4681 requested a finite two-player quantum parallel repetition entry as research solved
• ℹ️ Scope Conjecture-database curation; the underlying mathematical and Lean proof is OpenAI's.

Opened Formal Conjectures issue #4681 to propose the finite two-player quantum parallel repetition result from OpenAI's ten-proofs release for inclusion as @[category research solved]. The proposal links the official article and paper, the immutable full Lean proof, and its compact Comparator Challenges statement template.

• 🔗 Review (2026-08-12) KitaKen1 documented the open-status and weakened-target mismatch
• 🔗 Affected declaration the Formal Conjectures Part II target asks only for existence
• 🔗 Source problem the original Part II asks where the maximum occurs
• ℹ️ Scope Status and formalization-scope review; PR #4888 is separately listed as the Lean proof of the maximum-existence variant, and the source question locating a maximizer remains open.

Posted a detailed status and statement-scope review on Formal Conjectures issue #4839. The Erdős Problems page contains two questions: Cambie's counterexamples settle the unimodality question in Part I, but neither the existence of many local maxima nor the recorded n=3 Lean counterexample locates a global maximizer for general n, as requested by Part II. The review therefore explains why the page-level DISPROVED (LEAN) status reflects Part I and why Erdős Problem 692 as a whole should remain open. It also identifies a scope mismatch in Formal Conjectures: its Part II declaration asks only for an endpoint at which the maximum is attained, not where that endpoint is or how to characterize it. PR #4888 supplies a kernel-checked proof of this literal existence target, so the review proposes recording it as a separate solved variant while retaining the source Part II as research open.

• 🔗 Tracker opened (2026-08-12) KitaKen1 organized the statement-audit leads into issue #4896
• 🔗 Maintainer validation williamjblair checked six leads and confirmed the findings, with a scope refinement
• 🔗 Tracker expanded (2026-08-14) KitaKen1 added statement blockers for the Erdős 1208 and 190 open PRs
• 🔗 Downstream review guide PR #4899 incorporates audit examples and credits the lead/confirmed distinction
• ℹ️ Scope Repository-wide statement-audit triage and coordination. The unchecked entries remain possible misformalizations until individually verified; this service record is not a claim to have solved the underlying mathematical problems.

Opened Formal Conjectures issue #4896 to turn a broad statement audit into a checkable triage queue. Its 18 checklist lines cover source/statement mismatches, vacuous or degenerate boundary cases, answer-slot semantics, and blockers in open pull requests; it also links the existing dedicated trackers for Erdős 80, 319, and 769. The issue explicitly labels the entries as leads rather than asserting that every item is a confirmed bug, and records that the list was organized with AI assistance from longer working notes. Formal Conjectures maintainer williamjblair then checked Erdős 694, 195, and 887 and reported that all three findings were correct. He also confirmed the Erdős 940, Green 21, and Erdős 939 boundary-case leads, while narrowing exactly what the Erdős 939 witness establishes. The follow-up mathematical-review-guide PR #4899 incorporates examples from the audit and explicitly credits its distinction between unverified leads and confirmed defects. On 2026-08-14, the tracker was expanded with two open-PR blockers: PR #4258 proposes an all-dimension exponent for Erdős 1208 whose d=2 case conflicts with the fixed power saving in arXiv:2607.05374, and PR #3588 encodes only three-term rainbow progressions for Erdős 190 although the cited problem and solution concern rainbow k-term progressions.

• 🔗 Follow-up tracker (2026-08-13) KitaKen1 organized ten independently trackable statement-design leads
• 🔗 A211417 update (2026-08-16) added an explicit positive witness candidate and stated the current verification scope
• 🔗 Separate fixed-target submission PR #5010 proves four fixed A211417 divisibility statements, not the general declaration
• ℹ️ Scope Statement-design audit and repair proposal. Unchecked items remain possible misformalizations; the A211417 general proof is not counted as a formal proof until it is kernel-checked in Lean.

Opened Formal Conjectures issue #4923, with the repository's misformalization label, as a follow-up to issue #4896. Its independently checkable entries identify four exact self-answer patterns in Erdős 33, 329, 348, and 409(iii); three reflexive Big-O or Big-Theta answers in Erdős 422, 539, and 789; the zero-witness defect in OEIS A211417; and boundary or indexing problems in OEIS A111291 and A109074. On 2026-08-16, the A211417 entry was strengthened from a defect report to a proposed mathematical repair: the intended positive statement appears to hold with D(r)=lcm(1,…,r)^|{1≤i≤r : gcd(i,30)=1}|. The issue records the general proof as paper-complete but not yet Lean-checked, and distinguishes it from the four fixed divisibility statements submitted in PR #5010. The checklist remains a review queue rather than a claim that every underlying problem has been solved.

• 🔗 Batch audit (2026-08-16) KitaKen1 documented five independently checkable leads with explicit witnesses
• 🔗 Affected pull request PR #4946 proposes 45 conjectures from the auto_oeis branch
• 🔗 Maintainer outcome and follow-up invitation (2026-08-17) mo271 said all five findings were useful and fixed, noted upstream OEIS typos, and invited KitaKen1 to review PR #5016
• 🔗 Independent A374265 evidence public Lean artifact proves unboundedness for the apparently corresponding process
• ℹ️ Scope A sampled audit of five files in a 45-conjecture import, not a review of the whole PR. The five reported defects were subsequently acknowledged and fixed by mo271.

Performed a voluntary quality-control pass on Formal Conjectures PR #4946, which imports 45 conjectures from the auto_oeis branch. The audit did not claim exhaustive review and presented all findings as leads for independent checking. It supplied a concrete modular counterexample candidate to A357565 at (m,p,r)=(2,3,2); identified an apparent duplicated value in A383327, with direct enumeration suggesting the final 67 should be 69; found that A379240's helper named A376418 appears not to encode OEIS A376418 and maps 56 and 60 to the same triple although the target function distinguishes them; linked a public Lean proof of unboundedness apparently conflicting with A374265's affirmative boundedness statement; and observed that A363414's existential is already witnessed by n=0, suggesting a missing positivity condition. Formal Conjectures collaborator mo271 thanked KitaKen1 for the useful review, stated that all five had been fixed, specifically noted that the audit also caught typos upstream at OEIS, and then invited a review of the follow-up PR #5016.

• 🔗 Review invitation (2026-08-17) after fixing all five findings from the earlier batch, mo271 asked KitaKen1 to also review PR #5016
• 🔗 Full batch audit (2026-08-17) KitaKen1 supplied a file-by-file table of 30 concrete questions and proposed repairs, then separately listed three interpretation-sensitive points
• 🔗 Affected pull request PR #5016 proposes 97 new OEIS files in an 8,292-line Auto-OEIS batch
• 🔗 Concrete counterexample lead the audit records p=11 counterexamples to two A179537 declarations
• 🔗 Author response and fixes (2026-08-18) codrut3 called the review very useful, addressed the comments, and identified the remaining interpretation questions
• 🔗 Downstream A129365 solution (2026-08-18) KitaKen1 proved all four exact open targets after the quotient definition was repaired
• 🔗 Downstream A003625 formalization (2026-08-19) KitaKen1 kernel-formalized the classical irreducibility criterion and explicitly distinguished it from new mathematics
• ℹ️ Scope Statement and definition audit of the 97-file version reviewed at commit 811eb80. Findings have mixed outcomes: many were applied, some were narrowed or withdrawn after clarification, and others still need maintainer judgment. The later A129365 and A003625 proofs are counted separately, not as part of this service record.

After Formal Conjectures collaborator mo271 explicitly invited a follow-up review in PR #4946, performed a statement-fidelity audit of all 97 OEIS files proposed in PR #5016. The report lists 30 concrete questions with a corresponding repair suggestion for each, plus three further points explicitly separated as possible interpretation or file-splitting differences. Recurring defects include omitted conjectures, generalizations, minimality claims, and occurrence directions; empty sInf searches that silently become zero; natural-number division or conversion before integrality and nonnegativity are established; and uncharacterized axioms used in place of sequence definitions. It also gives sharper test cases, including a likely false n=0 boundary in A017666 and p=11 counterexamples suggesting reversed Legendre-symbol arguments in A179537. Other entries flag supplied finiteness assumptions, missing positivity or existence conditions, and source constants weakened to arbitrary ones. The PR author called the review very useful, applied the suggestions broadly, and explained the few places where known instances or interpretive choices were intentionally outside the open targets; KitaKen1 then narrowed or withdrew the corresponding objections. After A129365 was repaired to keep the quotient rational until integrality is proved, KitaKen1 also published proofs of all four of its open targets, recorded separately as a mathematical contribution. A second downstream project supplied a Lean proof of A003625's classical irreducibility criterion, recorded separately as a literature-backed formalization.