From f501d1f15912681d963c95977f7ff9dc4a87dda1 Mon Sep 17 00:00:00 2001
From: SproutSeeds <11943677+SproutSeeds@users.noreply.github.com>
Date: Wed, 1 Apr 2026 06:51:27 +0000
Subject: [PATCH] chore(data): refresh Erdos catalog snapshots

---
 .../data/erdos_open_problems.md               |  83 ++-
 .../data/erdos_problems.active.json           | 526 +++++++---------
 .../data/erdos_problems.all.json              | 572 ++++++++++--------
 .../data/erdos_problems.closed.json           | 267 ++++++--
 .../data/erdos_problems.open.json             | 526 +++++++---------
 5 files changed, 1046 insertions(+), 928 deletions(-)

diff --git a/packs/erdos-open-problems/data/erdos_open_problems.md b/packs/erdos-open-problems/data/erdos_open_problems.md
index 46e175f..426f7b2 100644
--- a/packs/erdos-open-problems/data/erdos_open_problems.md
+++ b/packs/erdos-open-problems/data/erdos_open_problems.md
@@ -1,8 +1,8 @@
 # Erdos Open Problems (Active Snapshot)
 
-- generated_at_utc: `2026-03-05T15:52:31Z`
+- generated_at_utc: `2026-04-01T06:51:20Z`
 - source_url: `https://erdosproblems.com/range/1-end`
-- total_open: `691`
+- total_open: `688`
 
 - [#1](https://erdosproblems.com/1) — OPEN | $500 | number theory, additive combinatorics — edited: 23 January 2026 — If $A\subseteq \{1,\ldots,N\}$ with $\lvert A\rvert=n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$...
 - [#3](https://erdosproblems.com/3) — OPEN | $5000 | number theory, additive combinatorics, arithmetic progressions — edited: 23 January 2026 — If $A\subseteq \mathbb{N}$ has $\sum_{n\in A}\frac{1}{n}=\infty$ then must $A$ contain arbitrarily long arithmetic progressions?
@@ -10,13 +10,13 @@
 - [#7](https://erdosproblems.com/7) — VERIFIABLE | $25 | number theory, covering systems — edited: 22 January 2026 — Is there a distinct covering system all of whose moduli are odd?
 - [#9](https://erdosproblems.com/9) — OPEN | number theory, additive basis, primes — edited: 20 January 2026 — Let $A$ be the set of all odd integers $\geq 1$ not of the form $p+2^{k}+2^l$ (where $k,l\geq 0$ and $p$ is prime). Is the upper density...
 - [#10](https://erdosproblems.com/10) — OPEN | number theory, additive basis, primes — edited: 24 January 2026 — Is there some $k$ such that every large integer is the sum of a prime and at most $k$ powers of 2?
-- [#11](https://erdosproblems.com/11) — FALSIFIABLE | number theory, additive basis — edited: 20 January 2026 — Is every large odd integer $n$ the sum of a squarefree number and a power of 2?
+- [#11](https://erdosproblems.com/11) — OPEN | number theory, additive basis — edited: 20 January 2026 — Is every large odd integer $n$ the sum of a squarefree number and a power of 2?
 - [#12](https://erdosproblems.com/12) — OPEN | number theory — Let $A$ be an infinite set such that there are no distinct $a,b,c\in A$ such that $a\mid (b+c)$ and $b,c>a$. Is there such an $A$ with\[\...
 - [#14](https://erdosproblems.com/14) — OPEN | number theory, sidon sets, additive combinatorics — edited: 14 September 2025 — Let $A\subseteq \mathbb{N}$. Let $B\subseteq \mathbb{N}$ be the set of integers which are representable in exactly one way as the sum of...
 - [#15](https://erdosproblems.com/15) — OPEN | number theory, primes — Is it true that\[\sum_{n=1}^\infty(-1)^n\frac{n}{p_n}\]converges, where $p_n$ is the sequence of primes?
 - [#17](https://erdosproblems.com/17) — OPEN | number theory, primes — edited: 28 December 2025 — Are there infinitely many primes $p$ such that every even number $n\leq p-3$ can be written as a difference of primes $n=q_1-q_2$ where $...
 - [#18](https://erdosproblems.com/18) — OPEN | $250 | number theory, divisors, factorials — edited: 20 January 2026 — We call $m$ practical if every integer $1\leq n<m$ is the sum of distinct divisors of $m$. If $m$ is practical then let $h(m)$ be such th...
-- [#20](https://erdosproblems.com/20) — OPEN | $1000 | combinatorics — edited: 25 January 2026 — Let $f(n,k)$ be minimal such that every family $\mathcal{F}$ of $n$-uniform sets with $\lvert \mathcal{F}\rvert \geq f(n,k)$ contains a $...
+- [#20](https://erdosproblems.com/20) — OPEN | $1000 | combinatorics — edited: 07 March 2026 — Let $f(n,k)$ be minimal such that every family $\mathcal{F}$ of $n$-uniform sets with $\lvert \mathcal{F}\rvert \geq f(n,k)$ contains a $...
 - [#23](https://erdosproblems.com/23) — FALSIFIABLE | graph theory — edited: 18 January 2026 — Can every triangle-free graph on $5n$ vertices be made bipartite by deleting at most $n^2$ edges?
 - [#25](https://erdosproblems.com/25) — OPEN | number theory — edited: 20 January 2026 — Let $1\leq n_1<n_2<\cdots$ be an arbitrary sequence of integers, each with an associated residue class $a_i\pmod{n_i}$. Let $A$ be the se...
 - [#28](https://erdosproblems.com/28) — OPEN | $500 | number theory, additive basis — edited: 23 January 2026 — If $A\subseteq \mathbb{N}$ is such that $A+A$ contains all but finitely many integers then $\limsup 1_A\ast 1_A(n)=\infty$.
@@ -33,7 +33,7 @@
 - [#44](https://erdosproblems.com/44) — OPEN | number theory, sidon sets, additive combinatorics — edited: 09 January 2026 — Let $N\geq 1$ and $A\subset \{1,\ldots,N\}$ be a Sidon set. Is it true that, for any $\epsilon>0$, there exist $M$ and $B\subset \{N+1,\l...
 - [#50](https://erdosproblems.com/50) — OPEN | $250 | number theory — Schoenberg proved that for every $c\in [0,1]$ the density of\[\{ n\in \mathbb{N} : \phi(n)<cn\}\]exists. Let this density be denoted by $...
 - [#51](https://erdosproblems.com/51) — OPEN | number theory — edited: 30 September 2025 — Is there an infinite set $A\subset \mathbb{N}$ such that for every $a\in A$ there is an integer $n$ such that $\phi(n)=a$, and yet if $n_...
-- [#52](https://erdosproblems.com/52) — OPEN | $250 | number theory, additive combinatorics — edited: 23 January 2026 — Let $A$ be a finite set of integers. Is it true that for every $\epsilon>0$\[\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A...
+- [#52](https://erdosproblems.com/52) — OPEN | $250 | number theory, additive combinatorics — edited: 23 March 2026 — Let $A$ be a finite set of integers. Is it true that for every $\epsilon>0$\[\max( \lvert A+A\rvert,\lvert AA\rvert)\gg_\epsilon \lvert A...
 - [#60](https://erdosproblems.com/60) — OPEN | graph theory, cycles — edited: 18 November 2025 — Does every graph on $n$ vertices with $>\mathrm{ex}(n;C_4)$ edges contain $\gg n^{1/2}$ many copies of $C_4$?
 - [#61](https://erdosproblems.com/61) — OPEN | graph theory — edited: 23 January 2026 — For any graph $H$ is there some $c=c(H)>0$ such that every graph $G$ on $n$ vertices that does not contain $H$ as an induced subgraph con...
 - [#62](https://erdosproblems.com/62) — OPEN | graph theory — edited: 23 January 2026 — If $G_1,G_2$ are two graphs with chromatic number $\aleph_1$ then must there exist a graph $G$ whose chromatic number is $4$ (or even $\a...
@@ -50,7 +50,7 @@
 - [#81](https://erdosproblems.com/81) — OPEN | graph theory — edited: 28 December 2025 — Let $G$ be a chordal graph on $n$ vertices - that is, $G$ has no induced cycles of length greater than $3$. Can the edges of $G$ be parti...
 - [#82](https://erdosproblems.com/82) — OPEN | graph theory — edited: 06 October 2025 — Let $F(n)$ be maximal such that every graph on $n$ vertices contains a regular induced subgraph on at least $F(n)$ vertices. Prove that $...
 - [#84](https://erdosproblems.com/84) — OPEN | graph theory, cycles — The cycle set of a graph $G$ on $n$ vertices is a set $A\subseteq \{3,\ldots,n\}$ such that there is a cycle in $G$ of length $\ell$ if a...
-- [#85](https://erdosproblems.com/85) — FALSIFIABLE | graph theory, ramsey theory — edited: 06 December 2025 — Let $n\geq 4$ and $f(n)$ be minimal such that every graph on $n$ vertices with minimal degree $\geq f(n)$ contains a $C_4$. Is it true th...
+- [#85](https://erdosproblems.com/85) — OPEN | graph theory, ramsey theory — edited: 06 December 2025 — Let $n\geq 4$ and $f(n)$ be minimal such that every graph on $n$ vertices with minimal degree $\geq f(n)$ contains a $C_4$. Is it true th...
 - [#86](https://erdosproblems.com/86) — OPEN | $100 | graph theory — edited: 27 December 2025 — Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Is it true that every subgraph...
 - [#87](https://erdosproblems.com/87) — OPEN | graph theory, ramsey theory — edited: 17 January 2026 — Let $\epsilon >0$. Is it true that, if $k$ is sufficiently large, then\[R(G)>(1-\epsilon)^kR(k)\]for every graph $G$ with chromatic numbe...
 - [#89](https://erdosproblems.com/89) — OPEN | $500 | geometry, distances — edited: 23 January 2026 — Does every set of $n$ distinct points in $\mathbb{R}^2$ determine $\gg n/\sqrt{\log n}$ many distinct distances?
@@ -66,19 +66,18 @@
 - [#102](https://erdosproblems.com/102) — OPEN | geometry — Let $c>0$ and $h_c(n)$ be such that for any $n$ points in $\mathbb{R}^2$ such that there are $\geq cn^2$ lines each containing more than...
 - [#103](https://erdosproblems.com/103) — OPEN | geometry, distances — Let $h(n)$ count the number of incongruent sets of $n$ points in $\mathbb{R}^2$ which minimise the diameter subject to the constraint tha...
 - [#104](https://erdosproblems.com/104) — OPEN | $100 | geometry — Given $n$ points in $\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$.
-- [#106](https://erdosproblems.com/106) — FALSIFIABLE | geometry — Draw $n$ squares inside the unit square with no common interior point. Let $f(n)$ be the maximum possible sum of the side-lengths of the...
+- [#106](https://erdosproblems.com/106) — FALSIFIABLE | geometry — edited: 06 March 2026 — Draw $n$ squares inside the unit square with no common interior point. Let $f(n)$ be the maximum possible sum of the side-lengths of the...
 - [#107](https://erdosproblems.com/107) — FALSIFIABLE | $500 | geometry, convex — edited: 23 January 2026 — Let $f(n)$ be minimal such that any $f(n)$ points in $\mathbb{R}^2$, no three on a line, contain $n$ points which form the vertices of a...
 - [#108](https://erdosproblems.com/108) — OPEN | graph theory, chromatic number, cycles — edited: 23 January 2026 — For every $r\geq 4$ and $k\geq 2$ is there some finite $f(k,r)$ such that every graph of chromatic number $\geq f(k,r)$ contains a subgra...
 - [#111](https://erdosproblems.com/111) — OPEN | graph theory, chromatic number, set theory — If $G$ is a graph let $h_G(n)$ be defined such that any subgraph of $G$ on $n$ vertices can be made bipartite after deleting at most $h_G...
 - [#112](https://erdosproblems.com/112) — OPEN | graph theory, ramsey theory — Let $k=k(n,m)$ be minimal such that any directed graph on $k$ vertices must contain either an independent set of size $n$ or a transitive...
-- [#114](https://erdosproblems.com/114) — OPEN | $250 | polynomials, analysis — edited: 23 January 2026 — If $p(z)\in\mathbb{C}[z]$ is a monic polynomial of degree $n$ then is the length of the curve $\{ z\in \mathbb{C} : \lvert p(z)\rvert=1\}...
+- [#114](https://erdosproblems.com/114) — FALSIFIABLE | $250 | polynomials, analysis — edited: 23 January 2026 — If $p(z)\in\mathbb{C}[z]$ is a monic polynomial of degree $n$ then is the length of the curve $\{ z\in \mathbb{C} : \lvert p(z)\rvert=1\}...
 - [#117](https://erdosproblems.com/117) — OPEN | group theory — edited: 23 January 2026 — Let $h(n)$ be minimal such that any group $G$ with the property that any subset of $>n$ elements contains some $x\neq y$ such that $xy=yx...
 - [#119](https://erdosproblems.com/119) — OPEN | $100 | analysis, polynomials — edited: 23 January 2026 — Let $z_i$ be an infinite sequence of complex numbers such that $\lvert z_i\rvert=1$ for all $i\geq 1$, and for $n\geq 1$ let\[p_n(z)=\pro...
 - [#120](https://erdosproblems.com/120) — OPEN | $100 | combinatorics — edited: 23 January 2026 — Let $A\subseteq\mathbb{R}$ be an infinite set. Must there be a set $E\subset \mathbb{R}$ of positive measure which does not contain any s...
 - [#122](https://erdosproblems.com/122) — OPEN | number theory — edited: 01 February 2026 — For which number theoretic functions $f$ is it true that, for any $F(n)$ such that $f(n)/F(n)\to 0$ for almost all $n$, there are infinit...
 - [#123](https://erdosproblems.com/123) — OPEN | $250 | number theory — edited: 20 January 2026 — Let $a,b,c\geq 1$ be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form $a^kb^lc^...
 - [#124](https://erdosproblems.com/124) — OPEN | number theory, base representations, complete sequences — edited: 01 December 2025 — For any $d\geq 1$ and $k\geq 0$ let $P(d,k)$ be the set of integers which are the sum of distinct powers $d^i$ with $i\geq k$. Let $3\leq...
-- [#125](https://erdosproblems.com/125) — OPEN | number theory, base representations — Let $A = \{ \sum\epsilon_k3^k : \epsilon_k\in \{0,1\}\}$ be the set of integers which have only the digits $0,1$ when written base $3$, a...
 - [#126](https://erdosproblems.com/126) — OPEN | $250 | number theory — Let $f(n)$ be maximal such that if $A\subseteq\mathbb{N}$ has $\lvert A\rvert=n$ then $\prod_{a\neq b\in A}(a+b)$ has at least $f(n)$ dis...
 - [#128](https://erdosproblems.com/128) — FALSIFIABLE | $250 | graph theory — edited: 31 October 2025 — Let $G$ be a graph with $n$ vertices such that every induced subgraph on $\geq \lfloor n/2\rfloor$ vertices has more than $n^2/50$ edges....
 - [#129](https://erdosproblems.com/129) — OPEN | graph theory, ramsey theory — Let $R(n;k,r)$ be the smallest $N$ such that if the edges of $K_N$ are $r$-coloured then there is a set of $n$ vertices which does not co...
@@ -100,13 +99,13 @@
 - [#155](https://erdosproblems.com/155) — OPEN | additive combinatorics, sidon sets — Let $F(N)$ be the size of the largest Sidon subset of $\{1,\ldots,N\}$. Is it true that for every $k\geq 1$ we have\[F(N+k)\leq F(N)+1\]f...
 - [#156](https://erdosproblems.com/156) — OPEN | sidon sets — Does there exist a maximal Sidon set $A\subset \{1,\ldots,N\}$ of size $O(N^{1/3})$?
 - [#158](https://erdosproblems.com/158) — OPEN | sidon sets — Let $A\subset \mathbb{N}$ be an infinite set such that, for any $n$, there are most $2$ solutions to $a+b=n$ with $a\leq b$. Must\[\limin...
-- [#159](https://erdosproblems.com/159) — OPEN | graph theory, ramsey theory — There exists some constant $c>0$ such that $$R(C_4,K_n) \ll n^{2-c}.$$
+- [#159](https://erdosproblems.com/159) — OPEN | $100 | graph theory, ramsey theory — edited: 07 March 2026 — There exists some constant $c>0$ such that $$R(C_4,K_n) \ll n^{2-c}.$$
 - [#160](https://erdosproblems.com/160) — OPEN | additive combinatorics, arithmetic progressions — edited: 02 December 2025 — Let $h(N)$ be the smallest $k$ such that $\{1,\ldots,N\}$ can be coloured with $k$ colours so that every four-term arithmetic progression...
 - [#161](https://erdosproblems.com/161) — OPEN | $500 | combinatorics, hypergraphs, ramsey theory, discrepancy — edited: 16 January 2026 — Let $\alpha\in[0,1/2)$ and $n,t\geq 1$. Let $F^{(t)}(n,\alpha)$ be the smallest $m$ such that we can $2$-colour the edges of the complete...
 - [#162](https://erdosproblems.com/162) — OPEN | combinatorics, ramsey theory, discrepancy — edited: 30 December 2025 — Let $\alpha>0$ and $n\geq 1$. Let $F(n,\alpha)$ be the largest $k$ such that there exists some 2-colouring of the edges of $K_n$ in which...
-- [#165](https://erdosproblems.com/165) — OPEN | $250 | graph theory, ramsey theory — edited: 28 December 2025 — Give an asymptotic formula for $R(3,k)$.
+- [#165](https://erdosproblems.com/165) — OPEN | $250 | graph theory, ramsey theory — edited: 07 March 2026 — Give an asymptotic formula for $R(3,k)$.
 - [#167](https://erdosproblems.com/167) — FALSIFIABLE | graph theory — edited: 13 October 2025 — If $G$ is a graph with at most $k$ edge disjoint triangles then can $G$ be made triangle-free after removing at most $2k$ edges?
-- [#168](https://erdosproblems.com/168) — OPEN | additive combinatorics — edited: 24 October 2025 — Let $F(N)$ be the size of the largest subset of $\{1,\ldots,N\}$ which does not contain any set of the form $\{n,2n,3n\}$. What is\[ \lim...
+- [#168](https://erdosproblems.com/168) — OPEN | additive combinatorics — edited: 23 March 2026 — Let $F(N)$ be the size of the largest subset of $\{1,\ldots,N\}$ which does not contain any set of the form $\{n,2n,3n\}$. What is\[ \lim...
 - [#169](https://erdosproblems.com/169) — OPEN | additive combinatorics, arithmetic progressions — Let $k\geq 3$ and $f(k)$ be the supremum of $\sum_{n\in A}\frac{1}{n}$ as $A$ ranges over all sets of positive integers which do not cont...
 - [#170](https://erdosproblems.com/170) — OPEN | additive combinatorics — Let $F(N)$ be the smallest possible size of $A\subset \{0,1,\ldots,N\}$ such that $\{0,1,\ldots,N\}\subset A-A$. Find the value of\[\lim_...
 - [#172](https://erdosproblems.com/172) — OPEN | additive combinatorics, ramsey theory — edited: 01 February 2026 — Is it true that in any finite colouring of $\mathbb{N}$ there exist arbitrarily large finite $A$ such that all sums and products of disti...
@@ -193,7 +192,7 @@
 - [#326](https://erdosproblems.com/326) — OPEN | number theory, additive basis — Let $A\subset \mathbb{N}$ be an additive basis of order $2$. Must there exist $B=\{b_1<b_2<\cdots\}\subseteq A$ which is also a basis suc...
 - [#327](https://erdosproblems.com/327) — OPEN | number theory, unit fractions — Suppose $A\subseteq \{1,\ldots,N\}$ is such that if $a,b\in A$ and $a\neq b$ then $a+b\nmid ab$. Can $A$ be 'substantially more' than the...
 - [#329](https://erdosproblems.com/329) — OPEN | number theory, sidon sets — edited: 18 November 2025 — Suppose $A\subseteq \mathbb{N}$ is a Sidon set. How large can\[\limsup_{N\to \infty}\frac{\lvert A\cap \{1,\ldots,N\}\rvert}{N^{1/2}}\]be?
-- [#330](https://erdosproblems.com/330) — OPEN | number theory, additive basis — edited: 08 December 2025 — Does there exist a minimal basis with positive density, say $A\subset\mathbb{N}$, such that for any $n\in A$ the (upper) density of integ...
+- [#330](https://erdosproblems.com/330) — OPEN | number theory, additive basis — edited: 31 March 2026 — Does there exist a minimal basis with positive density, say $A\subset\mathbb{N}$, such that for any $n\in A$ the (upper) density of integ...
 - [#332](https://erdosproblems.com/332) — OPEN | number theory — edited: 28 October 2025 — Let $A\subseteq \mathbb{N}$ and $D(A)$ be the set of those numbers which occur infinitely often as $a_1-a_2$ with $a_1,a_2\in A$. What co...
 - [#334](https://erdosproblems.com/334) — OPEN | number theory — Find the best function $f(n)$ such that every $n$ can be written as $n=a+b$ where both $a,b$ are $f(n)$-smooth (that is, are not divisibl...
 - [#335](https://erdosproblems.com/335) — OPEN | number theory, additive combinatorics — edited: 28 September 2025 — Let $d(A)$ denote the density of $A\subseteq \mathbb{N}$. Characterise those $A,B\subseteq \mathbb{N}$ with positive density such that\[d...
@@ -215,17 +214,17 @@
 - [#361](https://erdosproblems.com/361) — OPEN | number theory — edited: 17 October 2025 — Let $c>0$ and $n$ be some large integer. What is the size of the largest $A\subseteq \{1,\ldots,\lfloor cn\rfloor\}$ such that $n$ is not...
 - [#364](https://erdosproblems.com/364) — VERIFIABLE | number theory, powerful — edited: 20 December 2025 — Are there any triples of consecutive positive integers all of which are powerful (i.e. if $p\mid n$ then $p^2\mid n$)?
 - [#365](https://erdosproblems.com/365) — OPEN | number theory, powerful — edited: 31 October 2025 — Do all pairs of consecutive powerful numbers $n$ and $n+1$ come from solutions to Pell equations ? In other words, must either $n$ or $n+...
-- [#366](https://erdosproblems.com/366) — VERIFIABLE | number theory, powerful — edited: 20 December 2025 — Are there any 2-full $n$ such that $n+1$ is 3-full? That is, if $p\mid n$ then $p^2\mid n$ and if $p\mid n+1$ then $p^3\mid n+1$.
-- [#367](https://erdosproblems.com/367) — OPEN | number theory, powerful — edited: 08 February 2026 — Let $B_2(n)$ be the 2-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is...
+- [#366](https://erdosproblems.com/366) — VERIFIABLE | number theory, powerful — edited: 23 March 2026 — Are there any $2$-full $n$ such that $n+1$ is $3$-full? That is, if $p\mid n$ then $p^2\mid n$ and if $p\mid n+1$ then $p^3\mid n+1$.
+- [#367](https://erdosproblems.com/367) — OPEN | number theory, powerful — edited: 23 March 2026 — Let $B_2(n)$ be the $2$-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). I...
 - [#368](https://erdosproblems.com/368) — OPEN | number theory — How large is the largest prime factor of $n(n+1)$?
-- [#369](https://erdosproblems.com/369) — OPEN | number theory — Let $\epsilon>0$ and $k\geq 2$. Is it true that, for all sufficiently large $n$, there is a sequence of $k$ consecutive integers in $\{1,...
+- [#369](https://erdosproblems.com/369) — PROVED (LEAN) | number theory — Let $\epsilon>0$ and $k\geq 2$. Is it true that, for all sufficiently large $n$, there is a sequence of $k$ consecutive integers in $\{1,...
 - [#371](https://erdosproblems.com/371) — OPEN | number theory — edited: 23 January 2026 — Let $P(n)$ denote the largest prime factor of $n$. Show that the set of $n$ with $P(n)<P(n+1)$ has density $1/2$.
 - [#373](https://erdosproblems.com/373) — OPEN | number theory, factorials — edited: 29 January 2026 — Show that the equation\[n! = a_1!a_2!\cdots a_k!,\]with $n-1>a_1\geq a_2\geq \cdots \geq a_k\geq 2$, has only finitely many solutions.
 - [#374](https://erdosproblems.com/374) — OPEN | number theory — For any $m\in \mathbb{N}$, let $F(m)$ be the minimal $k\geq 2$ (if it exists) such that there are $a_1<\cdots <a_k=m$ with $a_1!\cdots a_...
 - [#375](https://erdosproblems.com/375) — FALSIFIABLE | number theory, primes — edited: 24 January 2026 — Is it true that for any $n,k\geq 1$, if $n+1,\ldots,n+k$ are all composite then there are distinct primes $p_1,\ldots,p_k$ such that $p_i...
 - [#376](https://erdosproblems.com/376) — OPEN | number theory, binomial coefficients, base representations — edited: 28 December 2025 — Are there infinitely many $n$ such that $\binom{2n}{n}$ is coprime to $105$?
 - [#377](https://erdosproblems.com/377) — OPEN | number theory, binomial coefficients — edited: 30 September 2025 — Is there some absolute constant $C>0$ such that\[\sum_{p\leq n}1_{p\nmid \binom{2n}{n}}\frac{1}{p}\leq C\]for all $n$ (where the summatio...
-- [#380](https://erdosproblems.com/380) — OPEN | number theory — We call an interval $[u,v]$ 'bad' if the greatest prime factor of $\prod_{u\leq m\leq v}m$ occurs with an exponent greater than $1$. Let...
+- [#380](https://erdosproblems.com/380) — PROVED | number theory — We call an interval $[u,v]$ 'bad' if the greatest prime factor of $\prod_{u\leq m\leq v}m$ occurs with an exponent greater than $1$. Let...
 - [#382](https://erdosproblems.com/382) — OPEN | number theory — Let $u\leq v$ be such that the largest prime dividing $\prod_{u\leq m\leq v}m$ appears with exponent at least $2$. Is it true that $v-u=v...
 - [#383](https://erdosproblems.com/383) — OPEN | number theory — 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)\]...
 - [#385](https://erdosproblems.com/385) — OPEN | number theory — Let\[F(n) = \max_{\substack{m<n\\ m\textrm{ composite}}} m+p(m),\]where $p(m)$ is the least prime divisor of $m$. Is it true that $F(n)>n...
@@ -237,7 +236,7 @@
 - [#393](https://erdosproblems.com/393) — OPEN | number theory, factorials — Let $f(n)$ denote the minimal $m\geq 1$ such that\[n! = a_1\cdots a_t\]with $a_1<\cdots <a_t=a_1+m$. What is the behaviour of $f(n)$?
 - [#394](https://erdosproblems.com/394) — OPEN | number theory — edited: 28 October 2025 — Let $t_k(n)$ denote the least $m$ such that\[n\mid m(m+1)(m+2)\cdots (m+k-1).\]Is it true that\[\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log...
 - [#396](https://erdosproblems.com/396) — OPEN | number theory, binomial coefficients — Is it true that for every $k$ there exists $n$ such that\[\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?\]
-- [#398](https://erdosproblems.com/398) — FALSIFIABLE | number theory, factorials — Are the only solutions to\[n!=x^2-1\]when $n=4,5,7$?
+- [#398](https://erdosproblems.com/398) — FALSIFIABLE | number theory, factorials — edited: 01 April 2026 — Are the only solutions to\[n!=x^2-1\]when $n=4,5,7$?
 - [#400](https://erdosproblems.com/400) — OPEN | number theory, factorials — For any $k\geq 2$ let $g_k(n)$ denote the maximum value of\[(a_1+\cdots+a_k)-n\]where $a_1,\ldots,a_k$ are integers such that $a_1!\cdots...
 - [#404](https://erdosproblems.com/404) — OPEN | number theory, factorials — edited: 29 September 2025 — 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 \...
 - [#406](https://erdosproblems.com/406) — OPEN | number theory, base representations — edited: 30 September 2025 — Is it true that there are only finitely many powers of $2$ which have only the digits $0$ and $1$ when written in base $3$?
@@ -254,8 +253,8 @@
 - [#420](https://erdosproblems.com/420) — OPEN | number theory — edited: 03 December 2025 — If $\tau(n)$ counts the number of divisors of $n$ then let\[F(f,n)=\frac{\tau((n+\lfloor f(n)\rfloor)!)}{\tau(n!)}.\]Is it true that\[\li...
 - [#421](https://erdosproblems.com/421) — OPEN | number theory — Is there a sequence $1\leq d_1<d_2<\cdots$ with density $1$ such that all products $\prod_{u\leq i\leq v}d_i$ are distinct?
 - [#422](https://erdosproblems.com/422) — OPEN | number theory — Let $f(1)=f(2)=1$ and for $n>2$\[f(n) = f(n-f(n-1))+f(n-f(n-2)).\]Does $f(n)$ miss infinitely many integers? What is its behaviour?
-- [#423](https://erdosproblems.com/423) — OPEN | number theory — edited: 16 January 2026 — Let $a_1=1$ and $a_2=2$ and for $k\geq 3$ choose $a_k$ to be the least integer $>a_{k-1}$ which is the sum of at least two consecutive te...
-- [#424](https://erdosproblems.com/424) — OPEN | number theory — Let $a_1=2$ and $a_2=3$ and continue the sequence by appending to $a_1,\ldots,a_n$ all possible values of $a_ia_j-1$ with $i\neq j$. Is i...
+- [#423](https://erdosproblems.com/423) — OPEN | number theory — edited: 23 March 2026 — Let $a_1=1$ and $a_2=2$ and for $k\geq 3$ choose $a_k$ to be the least integer $>a_{k-1}$ which is the sum of at least two consecutive te...
+- [#424](https://erdosproblems.com/424) — OPEN | number theory — edited: 31 March 2026 — Let $a_1=2$ and $a_2=3$ and continue the sequence by appending to $a_1,\ldots,a_n$ all possible values of $a_ia_j-1$ with $i\neq j$. Is i...
 - [#425](https://erdosproblems.com/425) — OPEN | number theory, sidon sets — edited: 28 December 2025 — 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...
 - [#428](https://erdosproblems.com/428) — OPEN | number theory, primes — Is there a set $A\subseteq \mathbb{N}$ such that, for infinitely many $n$, all of $n-a$ are prime for all $a\in A$ with $0<a<n$ and\[\lim...
 - [#430](https://erdosproblems.com/430) — OPEN | number theory — Fix some integer $n$ and define a decreasing sequence in $[1,n)$ by $a_1=n-1$ and, for $k\geq 2$, letting $a_k$ be the greatest integer i...
@@ -269,7 +268,6 @@
 - [#454](https://erdosproblems.com/454) — OPEN | number theory, primes — edited: 07 October 2025 — Let\[f(n) = \min_{i<n} (p_{n+i}+p_{n-i}),\]where $p_k$ is the $k$th prime. Is it true that\[\limsup_n (f(n)-2p_n)=\infty?\]
 - [#455](https://erdosproblems.com/455) — OPEN | number theory — edited: 07 October 2025 — Let $q_1<q_2<\cdots$ be a sequence of primes such that\[q_{n+1}-q_n\geq q_n-q_{n-1}.\]Must\[\lim_n \frac{q_n}{n^2}=\infty?\]
 - [#456](https://erdosproblems.com/456) — OPEN | number theory — edited: 07 October 2025 — Let $p_n$ be the smallest prime $\equiv 1\pmod{n}$ and let $m_n$ be the smallest integer such that $n\mid \phi(m_n)$. Is it true that $m_...
-- [#457](https://erdosproblems.com/457) — OPEN | number theory — edited: 07 October 2025 — Is there some $\epsilon>0$ such that there are infinitely many $n$ where all primes $p\leq (2+\epsilon)\log n$ divide\[\prod_{1\leq i\leq...
 - [#458](https://erdosproblems.com/458) — FALSIFIABLE | number theory, primes — edited: 07 October 2025 — Let $[1,\ldots,n]$ denote the least common multiple of $\{1,\ldots,n\}$. Is it true that, for all $k\geq 1$,\[[1,\ldots,p_{k+1}-1]< p_k[1...
 - [#460](https://erdosproblems.com/460) — OPEN | number theory — edited: 14 January 2026 — Let $a_0=0$ and $a_1=1$, and in general define $a_k$ to be the least integer $>a_{k-1}$ for which $(n-a_k,n-a_i)=1$ for all $0\leq i<k$....
 - [#461](https://erdosproblems.com/461) — OPEN | number theory, primes — edited: 28 October 2025 — Let $s_t(n)$ be the $t$-smooth component of $n$ - that is, the product of all primes $p$ (with multiplicity) dividing $n$ such that $p<t$...
@@ -281,13 +279,13 @@
 - [#470](https://erdosproblems.com/470) — OPEN | $10 | number theory, divisors — edited: 18 January 2026 — Call $n$ weird if $\sigma(n)\geq 2n$ and $n$ is not pseudoperfect, that is, it is not the sum of any set of its divisors. Are there any o...
 - [#472](https://erdosproblems.com/472) — OPEN | number theory — Given some initial finite sequence of primes $q_1<\cdots<q_m$ extend it so that $q_{n+1}$ is the smallest prime of the form $q_n+q_i-1$ f...
 - [#474](https://erdosproblems.com/474) — NOT PROVABLE | $100 | set theory, ramsey theory — edited: 01 February 2026 — Under what set theoretic assumptions is it true that $\mathbb{R}^2$ can be $3$-coloured such that, for every uncountable $A\subseteq \mat...
-- [#475](https://erdosproblems.com/475) — DECIDABLE | number theory, additive combinatorics — Let $p$ be a prime. Given any finite set $A\subseteq \mathbb{F}_p\backslash \{0\}$, is there always a rearrangement $A=\{a_1,\ldots,a_t\}...
+- [#475](https://erdosproblems.com/475) — DECIDABLE | number theory, additive combinatorics — edited: 05 March 2026 — Let $p$ be a prime. Given any finite set $A\subseteq \mathbb{F}_p\backslash \{0\}$, is there always a rearrangement $A=\{a_1,\ldots,a_t\}...
 - [#477](https://erdosproblems.com/477) — OPEN | number theory — edited: 29 December 2025 — Is there a polynomial $f:\mathbb{Z}\to \mathbb{Z}$ of degree at least $2$ and a set $A\subset \mathbb{Z}$ such that for any $n\in \mathbb...
 - [#478](https://erdosproblems.com/478) — OPEN | number theory, factorials — edited: 04 October 2025 — Let $p$ be a prime and\[A_p = \{ k! \pmod{p} : 1\leq k<p\}.\]Is it true that\[\lvert A_p\rvert \sim (1-\tfrac{1}{e})p?\]
 - [#479](https://erdosproblems.com/479) — OPEN | number theory — edited: 03 December 2025 — Is it true that, for all $k\neq 1$, there are infinitely many $n$ such that $2^n\equiv k\pmod{n}$?
 - [#483](https://erdosproblems.com/483) — OPEN | number theory, additive combinatorics, ramsey theory — edited: 14 October 2025 — Let $f(k)$ be the minimal $N$ such that if $\{1,\ldots,N\}$ is $k$-coloured then there is a monochromatic solution to $a+b=c$. Estimate $...
 - [#486](https://erdosproblems.com/486) — OPEN | number theory, primitive sets — edited: 12 January 2026 — Let $A\subseteq \mathbb{N}$, and for each $n\in A$ choose some $X_n\subseteq \mathbb{Z}/n\mathbb{Z}$. Let\[B = \{ m\in \mathbb{N} : m\not...
-- [#488](https://erdosproblems.com/488) — OPEN | number theory — edited: 31 December 2025 — Let $A$ be a finite set and\[B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.\]Is it true that, for every $m>n\geq \max(A)$,\[\frac{\l...
+- [#488](https://erdosproblems.com/488) — FALSIFIABLE | number theory — edited: 31 December 2025 — Let $A$ be a finite set and\[B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.\]Is it true that, for every $m>n\geq \max(A)$,\[\frac{\l...
 - [#489](https://erdosproblems.com/489) — OPEN | number theory — Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$. Let\[B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in...
 - [#495](https://erdosproblems.com/495) — OPEN | diophantine approximation, number theory — Let $\alpha,\beta \in \mathbb{R}$. Is it true that\[\liminf_{n\to \infty} n \| n\alpha \| \| n\beta\| =0\]where $\|x\|$ is the distance f...
 - [#500](https://erdosproblems.com/500) — OPEN | $500 | graph theory, hypergraphs, turan number — edited: 05 October 2025 — What is $\mathrm{ex}_3(n,K_4^3)$? That is, the largest number of $3$-edges which can placed on $n$ vertices so that there exists no $K_4^...
@@ -314,7 +312,7 @@
 - [#539](https://erdosproblems.com/539) — OPEN | number theory — edited: 22 January 2026 — Let $h(n)$ be such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the set\[\left\{ \frac{a}{(a,b)}: a,b\in A\right\}\]has size at...
 - [#544](https://erdosproblems.com/544) — OPEN | graph theory, ramsey theory — Show that\[R(3,k+1)-R(3,k)\to\infty\]as $k\to \infty$. Similarly, prove or disprove that\[R(3,k+1)-R(3,k)=o(k).\]
 - [#545](https://erdosproblems.com/545) — OPEN | graph theory, ramsey theory — edited: 02 December 2025 — Let $G$ be a graph with $m$ edges and no isolated vertices. Is the Ramsey number $R(G)$ maximised when $G$ is 'as complete as possible'?...
-- [#548](https://erdosproblems.com/548) — FALSIFIABLE | graph theory — edited: 23 January 2026 — Let $n\geq k+1$. Every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.
+- [#548](https://erdosproblems.com/548) — FALSIFIABLE | $100 | graph theory — edited: 07 March 2026 — Let $n\geq k+1$. Every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.
 - [#550](https://erdosproblems.com/550) — OPEN | graph theory, ramsey theory — Let $m_1\leq\cdots\leq m_k$ and $n$ be sufficiently large. If $T$ is a tree on $n$ vertices and $G$ is the complete multipartite graph wi...
 - [#552](https://erdosproblems.com/552) — OPEN | $100 | graph theory, ramsey theory — edited: 01 February 2026 — Determine the Ramsey number\[R(C_4,S_n),\]where $S_n=K_{1,n}$ is the star on $n+1$ vertices. In particular, is it true that, for any $c>0...
 - [#554](https://erdosproblems.com/554) — OPEN | graph theory, ramsey theory — edited: 08 February 2026 — Let $R_k(G)$ denote the minimal $m$ such that if the edges of $K_m$ are $k$-coloured then there is a monochromatic copy of $G$. Show that...
@@ -330,10 +328,10 @@
 - [#567](https://erdosproblems.com/567) — OPEN | graph theory, ramsey theory — edited: 18 January 2026 — Let $G$ be either $Q_3$ or $K_{3,3}$ or $H_5$ (the last formed by adding two vertex-disjoint chords to $C_5$). Is it true that, if $H$ ha...
 - [#568](https://erdosproblems.com/568) — OPEN | graph theory, ramsey theory — edited: 18 January 2026 — Let $G$ be a graph such that $R(G,T_n)\ll n$ for any tree $T_n$ on $n$ vertices and $R(G,K_n)\ll n^2$. Is it true that, for any $H$ with...
 - [#569](https://erdosproblems.com/569) — OPEN | graph theory, ramsey theory — edited: 18 January 2026 — Let $k\geq 1$. What is the best possible $c_k$ such that\[R(C_{2k+1},H)\leq c_k m\]for any graph $H$ on $m$ edges without isolated vertices?
-- [#571](https://erdosproblems.com/571) — OPEN | graph theory, turan number — edited: 18 January 2026 — Show that for any rational $\alpha \in [1,2)$ there exists a bipartite graph $G$ such that\[\mathrm{ex}(n;G)\asymp n^{\alpha}.\]
+- [#571](https://erdosproblems.com/571) — OPEN | graph theory, turan number — edited: 07 March 2026 — Show that for any rational $\alpha \in [1,2)$ there exists a bipartite graph $G$ such that\[\mathrm{ex}(n;G)\asymp n^{\alpha}.\]
 - [#572](https://erdosproblems.com/572) — OPEN | graph theory, turan number, cycles — edited: 18 January 2026 — Show that for $k\geq 3$\[\mathrm{ex}(n;C_{2k})\gg n^{1+\frac{1}{k}}.\]
 - [#573](https://erdosproblems.com/573) — OPEN | graph theory, turan number — edited: 18 January 2026 — Is it true that\[\mathrm{ex}(n;\{C_3,C_4\})\sim (n/2)^{3/2}?\]
-- [#574](https://erdosproblems.com/574) — OPEN | graph theory, turan number — edited: 18 January 2026 — Is it true that, for $k\geq 2$,\[\mathrm{ex}(n;\{C_{2k-1},C_{2k}\})=(1+o(1))(n/2)^{1+\frac{1}{k}}.\]
+- [#574](https://erdosproblems.com/574) — DISPROVED | graph theory, turan number — edited: 18 January 2026 — Is it true that, for $k\geq 2$,\[\mathrm{ex}(n;\{C_{2k-1},C_{2k}\})=(1+o(1))(n/2)^{1+\frac{1}{k}}.\]
 - [#575](https://erdosproblems.com/575) — OPEN | graph theory, turan number — edited: 18 January 2026 — If $\mathcal{F}$ is a finite set of finite graphs then $\mathrm{ex}(n;\mathcal{F})$ is the maximum number of edges a graph on $n$ vertice...
 - [#576](https://erdosproblems.com/576) — OPEN | graph theory, turan number — edited: 18 January 2026 — Let $Q_k$ be the $k$-dimensional hypercube graph (so that $Q_k$ has $2^k$ vertices and $k2^{k-1}$ edges). Determine the behaviour of\[\ma...
 - [#579](https://erdosproblems.com/579) — OPEN | graph theory, turan number — Let $\delta>0$. If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no $K_{2,2,2}$ and at least $\delta n^2$ edges then...
@@ -353,7 +351,7 @@
 - [#601](https://erdosproblems.com/601) — OPEN | $500 | graph theory, set theory — For which limit ordinals $\alpha$ is it true that if $G$ is a graph with vertex set $\alpha$ then $G$ must have either an infinite path o...
 - [#602](https://erdosproblems.com/602) — OPEN | combinatorics, set theory — Let $(A_i)$ be a family of sets with $\lvert A_i\rvert=\aleph_0$ for all $i$, such that for any $i\neq j$ we have $\lvert A_i\cap A_j\rve...
 - [#603](https://erdosproblems.com/603) — OPEN | combinatorics, set theory — edited: 28 December 2025 — 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 cardi...
-- [#604](https://erdosproblems.com/604) — OPEN | $500 | geometry, distances — edited: 15 October 2025 — Given $n$ distinct points $A\subset\mathbb{R}^2$ must there be a point $x\in A$ such that\[\#\{ d(x,y) : y \in A\} \gg n^{1-o(1)}?\]Or ev...
+- [#604](https://erdosproblems.com/604) — OPEN | $500 | geometry, distances — edited: 23 March 2026 — Given $n$ distinct points $A\subset\mathbb{R}^2$ must there be a point $x\in A$ such that\[\#\{ d(x,y) : y \in A\} \gg n^{1-o(1)}?\]Or ev...
 - [#609](https://erdosproblems.com/609) — OPEN | graph theory, ramsey theory — Let $f(n)$ be the minimal $m$ such that if the edges of $K_{2^n+1}$ are coloured with $n$ colours then there must be a monochromatic odd...
 - [#610](https://erdosproblems.com/610) — OPEN | graph theory — edited: 02 December 2025 — For a graph $G$ let $\tau(G)$ denote the minimal number of vertices that include at least one from each maximal clique of $G$ (sometimes...
 - [#611](https://erdosproblems.com/611) — OPEN | graph theory — For a graph $G$ let $\tau(G)$ denote the minimal number of vertices that include at least one from each maximal clique of $G$ (sometimes...
@@ -379,7 +377,6 @@
 - [#643](https://erdosproblems.com/643) — OPEN | graph theory, hypergraphs — edited: 26 October 2025 — Let $f(n;t)$ be minimal such that if a $t$-uniform hypergraph on $n$ vertices contains at least $f(n;t)$ edges then there must be four ed...
 - [#644](https://erdosproblems.com/644) — OPEN | combinatorics — Let $f(k,r)$ be minimal such that if $A_1,A_2,\ldots$ is a family of sets, all of size $k$, such that for every collection of $r$ of the...
 - [#647](https://erdosproblems.com/647) — VERIFIABLE | $44 | number theory — edited: 05 October 2025 — 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?\]
-- [#650](https://erdosproblems.com/650) — OPEN | number theory — Let $f(m)$ be such that if $A\subseteq \{1,\ldots,N\}$ has $\lvert A\rvert=m$ then every interval in $[1,\infty)$ of length $2N$ contains...
 - [#653](https://erdosproblems.com/653) — OPEN | geometry, distances — Let $x_1,\ldots,x_n\in \mathbb{R}^2$ and let $R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}$, where the points are ordered such that\[R(x_...
 - [#654](https://erdosproblems.com/654) — OPEN | geometry, distances — edited: 01 February 2026 — Let $f(n)$ be such that, given any $x_1,\ldots,x_n\in \mathbb{R}^2$ with no four points on a circle, there exists some $x_i$ with at leas...
 - [#655](https://erdosproblems.com/655) — OPEN | geometry, distances — Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at le...
@@ -402,7 +399,7 @@
 - [#680](https://erdosproblems.com/680) — OPEN | number theory, primes — Is it true that, for all sufficiently large $n$, there exists some $k$ such that\[p(n+k)>k^2+1,\]where $p(m)$ denotes the least prime fac...
 - [#681](https://erdosproblems.com/681) — OPEN | number theory, primes — edited: 01 February 2026 — Is it true that for all large $n$ there exists $k$ such that $n+k$ is composite and\[p(n+k)>k^2,\]where $p(m)$ is the least prime factor...
 - [#683](https://erdosproblems.com/683) — OPEN | number theory, primes, binomial coefficients — edited: 31 December 2025 — Is it true that for every $1\leq k\leq n$ the largest prime divisor of $\binom{n}{k}$, say $P(\binom{n}{k})$, satisfies\[P\left(\binom{n}...
-- [#684](https://erdosproblems.com/684) — OPEN | number theory, primes, binomial coefficients — edited: 23 January 2026 — For $0\leq k\leq n$ write\[\binom{n}{k} = uv\]where the only primes dividing $u$ are in $[2,k]$ and the only primes dividing $v$ are in $...
+- [#684](https://erdosproblems.com/684) — OPEN | number theory, primes, binomial coefficients — edited: 01 April 2026 — For $0\leq k\leq n$ write\[\binom{n}{k} = uv\]where the only primes dividing $u$ are in $[2,k]$ and the only primes dividing $v$ are in $...
 - [#685](https://erdosproblems.com/685) — OPEN | number theory, primes, binomial coefficients — Let $\epsilon>0$ and $n$ be large depending on $\epsilon$. Is it true that for all $n^\epsilon<k\leq n^{1-\epsilon}$ the number of distin...
 - [#686](https://erdosproblems.com/686) — OPEN | number theory — Can every integer $N\geq 2$ be written as\[N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some $k\geq 2$ and $m\geq...
 - [#687](https://erdosproblems.com/687) — OPEN | $1000 | number theory — edited: 06 December 2025 — Let $Y(x)$ be the maximal $y$ such that there exists a choice of congruence classes $a_p$ for all primes $p\leq x$ such that every intege...
@@ -420,11 +417,11 @@
 - [#704](https://erdosproblems.com/704) — OPEN | graph theory, geometry, chromatic number — Let $G_n$ be the unit distance graph in $\mathbb{R}^n$, with two vertices joined by an edge if and only if the distance between them is $...
 - [#706](https://erdosproblems.com/706) — OPEN | graph theory, chromatic number — Let $L(r)$ be such that if $G$ is a graph formed by taking a finite set of points $P$ in $\mathbb{R}^2$ and some set $A\subset (0,\infty)...
 - [#708](https://erdosproblems.com/708) — OPEN | $100 | number theory — Let $g(n)$ be minimal such that for any $A\subseteq [2,\infty)\cap \mathbb{N}$ with $\lvert A\rvert =n$ and any set $I$ of $\max(A)$ cons...
-- [#709](https://erdosproblems.com/709) — OPEN | number theory — Let $f(n)$ be minimal such that, for any $A=\{a_1,\ldots,a_n\}\subseteq [2,\infty)\cap\mathbb{N}$ of size $n$, in any interval $I$ of $f(...
+- [#709](https://erdosproblems.com/709) — OPEN | number theory — edited: 23 March 2026 — Let $f(n)$ be minimal such that, for any $A=\{a_1,\ldots,a_n\}\subseteq [2,\infty)\cap\mathbb{N}$ of size $n$, in any interval $I$ of $f(...
 - [#710](https://erdosproblems.com/710) — OPEN | $78 | number theory — Let $f(n)$ be minimal such that in $(n,n+f(n))$ there exist distinct integers $a_1,\ldots,a_n$ such that $k\mid a_k$ for all $1\leq k\leq...
 - [#711](https://erdosproblems.com/711) — OPEN | $78 | number theory — edited: 11 January 2026 — Let $f(n,m)$ be minimal such that in $(m,m+f(n,m))$ there exist distinct integers $a_1,\ldots,a_n$ such that $k\mid a_k$ for all $1\leq k...
 - [#712](https://erdosproblems.com/712) — OPEN | $500 | graph theory, turan number, hypergraphs — edited: 05 October 2025 — Determine, for any $k>r>2$, the value of\[\frac{\mathrm{ex}_r(n,K_k^r)}{\binom{n}{r}},\]where $\mathrm{ex}_r(n,K_k^r)$ is the largest num...
-- [#713](https://erdosproblems.com/713) — OPEN | $500 | graph theory, turan number — edited: 06 October 2025 — Is it true that, for every bipartite graph $G$, there exists some $\alpha\in [1,2)$ and $c>0$ such that\[\mathrm{ex}(n;G)\sim cn^\alpha?\...
+- [#713](https://erdosproblems.com/713) — OPEN | $500 | graph theory, turan number — edited: 07 March 2026 — Is it true that, for every bipartite graph $G$, there exists some $\alpha\in [1,2)$ and $c>0$ such that\[\mathrm{ex}(n;G)\sim cn^\alpha?\...
 - [#714](https://erdosproblems.com/714) — OPEN | graph theory, turan number — edited: 23 January 2026 — Is it true that\[\mathrm{ex}(n; K_{r,r}) \gg n^{2-1/r}?\]
 - [#719](https://erdosproblems.com/719) — OPEN | graph theory, hypergraphs — Let $\mathrm{ex}_r(n;K_{r+1}^r)$ be the maximum number of $r$-edges that can be placed on $n$ vertices without forming a $K_{r+1}^r$ (the...
 - [#723](https://erdosproblems.com/723) — FALSIFIABLE | combinatorics — If there is a finite projective plane of order $n$ then must $n$ be a prime power? A finite projective plane of order $n$ is a collection...
@@ -439,7 +436,7 @@
 - [#738](https://erdosproblems.com/738) — OPEN | graph theory, chromatic number — If $G$ has infinite chromatic number and is triangle-free (contains no $K_3$) then must $G$ contain every tree as an induced subgraph?
 - [#739](https://erdosproblems.com/739) — NOT PROVABLE | graph theory, chromatic number — edited: 01 October 2025 — Let $\mathfrak{m}$ be an infinite cardinal and $G$ be a graph with chromatic number $\mathfrak{m}$. Is it true that, for every infinite c...
 - [#740](https://erdosproblems.com/740) — OPEN | graph theory, chromatic number — Let $\mathfrak{m}$ be an infinite cardinal and $G$ be a graph with chromatic number $\mathfrak{m}$. Let $r\geq 1$. Must $G$ contain a sub...
-- [#741](https://erdosproblems.com/741) — OPEN | additive combinatorics — Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $...
+- [#741](https://erdosproblems.com/741) — OPEN | additive combinatorics — edited: 01 April 2026 — Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive (upper) density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_...
 - [#743](https://erdosproblems.com/743) — FALSIFIABLE | graph theory — Let $T_2,\ldots,T_n$ be a collection of trees such that $T_k$ has $k$ vertices. Can we always write $K_n$ as the edge disjoint union of t...
 - [#749](https://erdosproblems.com/749) — OPEN | additive combinatorics — Let $\epsilon>0$. Does there exist $A\subseteq \mathbb{N}$ such that the lower density of $A+A$ is at least $1-\epsilon$ and yet $1_A\ast...
 - [#750](https://erdosproblems.com/750) — OPEN | graph theory, chromatic number — edited: 14 October 2025 — Let $f(m)$ be some function such that $f(m)\to \infty$ as $m\to \infty$. Does there exist a graph $G$ of infinite chromatic number such t...
@@ -496,7 +493,7 @@
 - [#852](https://erdosproblems.com/852) — OPEN | number theory, primes — Let $d_n=p_{n+1}-p_n$, where $p_n$ is the $n$th prime. Let $h(x)$ be maximal such that for some $n<x$ the numbers $d_n,d_{n+1},\ldots,d_{...
 - [#853](https://erdosproblems.com/853) — OPEN | number theory, primes — Let $d_n=p_{n+1}-p_n$, where $p_n$ is the $n$th prime. Let $r(x)$ be the smallest even integer $t$ such that $d_n=t$ has no solutions for...
 - [#854](https://erdosproblems.com/854) — OPEN | number theory — edited: 04 November 2025 — Let $n_k$ denote the $k$th primorial, i.e. the product of the first $k$ primes. If $1=a_1<a_2<\cdots a_{\phi(n_k)}=n_k-1$ is the sequence...
-- [#855](https://erdosproblems.com/855) — FALSIFIABLE | number theory, primes — edited: 12 January 2026 — If $\pi(x)$ counts the number of primes in $[1,x]$ then is it true that (for large $x$ and $y$)\[\pi(x+y) \leq \pi(x)+\pi(y)?\]
+- [#855](https://erdosproblems.com/855) — OPEN | number theory, primes — edited: 12 January 2026 — If $\pi(x)$ counts the number of primes in $[1,x]$ then is it true that (for large $x$ and $y$)\[\pi(x+y) \leq \pi(x)+\pi(y)?\]
 - [#856](https://erdosproblems.com/856) — OPEN | number theory — edited: 18 January 2026 — Let $k\geq 3$ and $f_k(N)$ be the maximum value of $\sum_{n\in A}\frac{1}{n}$, where $A$ ranges over all subsets of $\{1,\ldots,N\}$ whic...
 - [#857](https://erdosproblems.com/857) — OPEN | combinatorics — Let $m=m(n,k)$ be minimal such that in any collection of sets $A_1,\ldots,A_m\subseteq \{1,\ldots,n\}$ there must exist a sunflower of si...
 - [#858](https://erdosproblems.com/858) — OPEN | number theory, primitive sets — Let $A\subseteq \{1,\ldots,N\}$ be such that there is no solution to $at=b$ with $a,b\in A$ and the smallest prime factor of $t$ is $>a$....
@@ -516,7 +513,6 @@
 - [#879](https://erdosproblems.com/879) — OPEN | number theory — Call a set $S\subseteq \{1,\ldots,n\}$ admissible if $(a,b)=1$ for all $a\neq b\in S$. Let\[G(n) = \max_{S\subseteq \{1,\ldots,n\}} \sum_...
 - [#881](https://erdosproblems.com/881) — OPEN | number theory, additive basis — Let $A\subset\mathbb{N}$ be an additive basis of order $k$ which is minimal, in the sense that if $B\subset A$ is any infinite set then $...
 - [#883](https://erdosproblems.com/883) — OPEN | number theory, graph theory — edited: 24 October 2025 — For $A\subseteq \{1,\ldots,n\}$ let $G(A)$ be the graph with vertex set $A$, where two integers are joined by an edge if they are coprime...
-- [#884](https://erdosproblems.com/884) — OPEN | number theory, divisors — Is it true that, for any $n$, if $d_1<\cdots <d_t$ are the divisors of $n$, then\[\sum_{1\leq i<j\leq t}\frac{1}{d_j-d_i} \ll 1+\sum_{1\l...
 - [#885](https://erdosproblems.com/885) — OPEN | number theory, divisors — For integer $n\geq 1$ we define the factor difference set of $n$ by\[D(n) = \{\lvert a-b\rvert : n=ab\}.\]Is it true that, for every $k\g...
 - [#886](https://erdosproblems.com/886) — OPEN | number theory, divisors — edited: 01 February 2026 — Let $\epsilon>0$. Is it true that, for all large $n$, the number of divisors of $n$ in $(n^{1/2},n^{1/2}+n^{1/2-\epsilon})$ is $O_\epsilo...
 - [#887](https://erdosproblems.com/887) — OPEN | number theory, divisors — Is there an absolute constant $K$ such that, for every $C>0$, if $n$ is sufficiently large then $n$ has at most $K$ divisors in $(n^{1/2}...
@@ -567,7 +563,7 @@
 - [#961](https://erdosproblems.com/961) — OPEN | number theory — Let $f(k)$ be the minimal $n$ such that every set of $n$ consecutive integers $>k$ contains an integer divisible by a prime $>k$. Estimat...
 - [#962](https://erdosproblems.com/962) — OPEN | number theory — edited: 30 December 2025 — Let $k(n)$ be the maximal $k$ such that there exists $m\leq n$ such that each of the integers\[m+1,\ldots,m+k\]are divisible by at least...
 - [#963](https://erdosproblems.com/963) — OPEN | number theory — edited: 23 January 2026 — Let $f(n)$ be the maximal $k$ such that in any set $A\subset \mathbb{R}$ of size $n$ there is a subset $B\subseteq A$ of size $\lvert B\r...
-- [#968](https://erdosproblems.com/968) — OPEN | number theory — Let $u_n=p_n/n$, where $p_n$ is the $n$th prime. Does the set of $n$ such that $u_n<u_{n+1}$ have positive density?
+- [#968](https://erdosproblems.com/968) — OPEN | number theory — edited: 31 March 2026 — Let $u_n=p_n/n$, where $p_n$ is the $n$th prime. Does the set of $n$ such that $u_n<u_{n+1}$ have positive density?
 - [#969](https://erdosproblems.com/969) — OPEN | number theory — edited: 19 October 2025 — Let $Q(x)$ count the number of squarefree integers in $[1,x]$. Determine the order of magnitude in the error term in the asymptotic\[Q(x)...
 - [#970](https://erdosproblems.com/970) — OPEN | number theory — Let $h(k)$ be Jacobsthal's function, defined to as the minimal $m$ such that, if $n$ has at most $k$ prime factors, then in any set of $m...
 - [#971](https://erdosproblems.com/971) — OPEN | number theory — Let $p(a,d)$ be the least prime congruent to $a\pmod{d}$. Does there exist a constant $c>0$ such that, for all large $d$,\[p(a,d) > (1+c)...
@@ -575,7 +571,7 @@
 - [#973](https://erdosproblems.com/973) — OPEN | analysis — edited: 23 January 2026 — Does there exist a constant $C>1$ such that, for every $n\geq 2$, there exists a sequence $z_i\in \mathbb{C}$ with $z_1=1$ and $\lvert z_...
 - [#975](https://erdosproblems.com/975) — OPEN | number theory, divisors, polynomials — edited: 27 December 2025 — Let $f\in \mathbb{Z}[x]$ be an irreducible non-constant polynomial such that $f(n)\geq 1$ for all large $n\in\mathbb{N}$. Does there exis...
 - [#976](https://erdosproblems.com/976) — OPEN | number theory — edited: 01 February 2026 — Let $f\in \mathbb{Z}[x]$ be an irreducible polynomial of degree $d\geq 2$. Let $F_f(n)$ be maximal such that there exists $1\leq m\leq n$...
-- [#978](https://erdosproblems.com/978) — OPEN | number theory — edited: 05 March 2026 — Let $f\in \mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\neq 2^l$ for any $l\geq 1$) such that the lead...
+- [#978](https://erdosproblems.com/978) — OPEN | number theory — edited: 31 March 2026 — Let $f\in \mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\neq 2^l$ for any $l\geq 1$) such that the lead...
 - [#979](https://erdosproblems.com/979) — OPEN | number theory — edited: 19 September 2025 — Let $k\geq 2$, and let $f_k(n)$ count the number of solutions to\[n=p_1^k+\cdots+p_k^k,\]where the $p_i$ are prime numbers. Is it true th...
 - [#982](https://erdosproblems.com/982) — FALSIFIABLE | geometry, convex, distances — edited: 19 October 2025 — If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then some vertex has at least $\lfloor \frac{n}{2}\rfloor$ different dista...
 - [#983](https://erdosproblems.com/983) — OPEN | number theory — edited: 18 January 2026 — Let $n\geq 2$ and $\pi(n)<k\leq n$. Let $f(k,n)$ be the smallest integer $r$ such that in any $A\subseteq \{1,\ldots,n\}$ of size $\lvert...
@@ -586,7 +582,6 @@
 - [#993](https://erdosproblems.com/993) — FALSIFIABLE | graph theory — edited: 01 February 2026 — The independent set sequence of any tree or forest is unimodal. In other words, if $i_k(G)$ counts the number of independent sets of vert...
 - [#995](https://erdosproblems.com/995) — OPEN | analysis, discrepancy — Let $n_1<n_2<\cdots$ be a lacunary sequence of integers and $f\in L^2([0,1])$. Estimate the growth of, for almost all $\alpha$,\[\sum_{1\...
 - [#996](https://erdosproblems.com/996) — OPEN | analysis — Let $n_1<n_2<\cdots$ be a lacunary sequence of integers, and let $f\in L^2([0,1])$. Let $f_n$ be the $n$th partial sum of the Fourier ser...
-- [#997](https://erdosproblems.com/997) — OPEN | analysis, discrepancy, primes — Call $x_1,x_2,\ldots \in (0,1)$ well-distributed if, for every $\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and interva...
 - [#1002](https://erdosproblems.com/1002) — OPEN | analysis, diophantine approximation — For any $0<\alpha<1$, let\[f(\alpha,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}-\{ \alpha k\}).\]Does $f(\alpha,n)$ have an asym...
 - [#1003](https://erdosproblems.com/1003) — OPEN | number theory — edited: 31 October 2025 — Are there infinitely many solutions to $\phi(n)=\phi(n+1)$, where $\phi$ is the Euler totient function?
 - [#1004](https://erdosproblems.com/1004) — OPEN | number theory — Let $c>0$. If $x$ is sufficiently large then does there exist $n\leq x$ such that the values of $\phi(n+k)$ are all distinct for $1\leq k...
@@ -598,7 +593,7 @@
 - [#1017](https://erdosproblems.com/1017) — OPEN | graph theory — edited: 28 December 2025 — Let $f(n,k)$ be such that every graph on $n$ vertices and $k$ edges can be partitioned into at most $f(n,k)$ edge-disjoint complete graph...
 - [#1020](https://erdosproblems.com/1020) — FALSIFIABLE | graph theory, hypergraphs — edited: 28 December 2025 — Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges. For all $...
 - [#1029](https://erdosproblems.com/1029) — OPEN | $100 | graph theory, ramsey theory — If $R(k)$ is the Ramsey number for $K_k$, the minimal $n$ such that every $2$-colouring of the edges of $K_n$ contains a monochromatic co...
-- [#1030](https://erdosproblems.com/1030) — OPEN | graph theory, ramsey theory — edited: 03 December 2025 — If $R(k,l)$ is the Ramsey number then prove the existence of some $c>0$ such that\[\lim_k \frac{R(k+1,k)}{R(k,k)}> 1+c.\]
+- [#1030](https://erdosproblems.com/1030) — OPEN | graph theory, ramsey theory — edited: 23 March 2026 — Let $R(k,l)$ be the usual Ramsey number: the smallest $n$ such that if the edges of $K_n$ are coloured red and blue then there exists eit...
 - [#1032](https://erdosproblems.com/1032) — OPEN | graph theory, chromatic number — edited: 23 January 2026 — We say that a graph is $4$-chromatic critical if it has chromatic number $4$, and removing any edge decreases the chromatic number to $3$...
 - [#1033](https://erdosproblems.com/1033) — OPEN | graph theory — Let $h(n)$ be such that every graph on $n$ vertices with $>n^2/4$ many edges contains a triangle whose vertices have degrees summing to a...
 - [#1035](https://erdosproblems.com/1035) — OPEN | graph theory — Is there a constant $c>0$ such that every graph on $2^n$ vertices with minimum degree $>(1-c)2^n$ contains the $n$-dimensional hypercube...
@@ -606,7 +601,7 @@
 - [#1039](https://erdosproblems.com/1039) — OPEN | analysis, polynomials — edited: 27 December 2025 — 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 d...
 - [#1040](https://erdosproblems.com/1040) — OPEN | analysis — edited: 01 February 2026 — Let $F\subseteq \mathbb{C}$ be a closed infinite set, and let $\mu(F)$ be the infimum of\[\lvert \{ z: \lvert f(z)\rvert < 1\}\rvert,\]as...
 - [#1041](https://erdosproblems.com/1041) — FALSIFIABLE | analysis, polynomials — edited: 06 December 2025 — Let $f(z)=\prod_{i=1}^n(z-z_i)\in \mathbb{C}[z]$ with $\lvert z_i\rvert < 1$ for all $i$. Must there always exist a path of length less t...
-- [#1045](https://erdosproblems.com/1045) — FALSIFIABLE | analysis — edited: 30 December 2025 — Let $z_1,\ldots,z_n\in \mathbb{C}$ with $\lvert z_i-z_j\rvert\leq 2$ for all $i,j$, and\[\Delta(z_1,\ldots,z_n)=\prod_{i\neq j}\lvert z_i...
+- [#1045](https://erdosproblems.com/1045) — OPEN | analysis — edited: 30 December 2025 — Let $z_1,\ldots,z_n\in \mathbb{C}$ with $\lvert z_i-z_j\rvert\leq 2$ for all $i,j$, and\[\Delta(z_1,\ldots,z_n)=\prod_{i\neq j}\lvert z_i...
 - [#1049](https://erdosproblems.com/1049) — OPEN | irrationality — edited: 28 September 2025 — Let $t>1$ be a rational number. Is\[\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n}\]irrational, where $\tau(n)$ c...
 - [#1052](https://erdosproblems.com/1052) — OPEN | $10 | number theory — edited: 28 September 2025 — A unitary divisor of $n$ is $d\mid n$ such that $(d,n/d)=1$. A number $n\geq 1$ is a unitary perfect number if it is the sum of its unita...
 - [#1053](https://erdosproblems.com/1053) — OPEN | number theory — Call a number $k$-perfect if $\sigma(n)=kn$, where $\sigma(n)$ is the sum of the divisors of $n$. Must $k=o(\log\log n)$?
@@ -664,12 +659,11 @@
 - [#1138](https://erdosproblems.com/1138) — OPEN | number theory, primes — edited: 23 January 2026 — Let $x/2<y<x$ and $C>1$. If $d=\max_{p_n<x} (p_{n+1}-p_n)$, where $p_n$ denotes the $n$th prime, then is it true that\[\pi(y+Cd)-\pi(y)\s...
 - [#1139](https://erdosproblems.com/1139) — OPEN | number theory, primes — edited: 23 January 2026 — Let $1\leq u_1<u_2<\cdots$ be the sequence of integers with at most $2$ prime factors. Is it true that\[\limsup \frac{u_{k+1}-u_k}{\log k...
 - [#1141](https://erdosproblems.com/1141) — OPEN | number theory, primes — edited: 26 January 2026 — Are there infinitely many $n$ such that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2<n$?
-- [#1142](https://erdosproblems.com/1142) — OPEN | number theory, primes — edited: 23 January 2026 — Are there infinitely many $n$ (or any $n>105$) such that $n-2^k$ is prime for all $1<2^k<n$?
+- [#1142](https://erdosproblems.com/1142) — OPEN | number theory, primes — edited: 05 March 2026 — Are there infinitely many $n$ (or any $n>105$) such that $n-2^k$ is prime for all $1<2^k<n$?
 - [#1143](https://erdosproblems.com/1143) — OPEN | number theory, primes — edited: 23 January 2026 — Let $p_1<\cdots<p_u$ be primes and let $k\geq 1$. Let $F_k(p_1,\ldots,p_u)$ be such that every interval of $k$ positive integers contains...
 - [#1144](https://erdosproblems.com/1144) — OPEN | number theory, probability — edited: 26 January 2026 — Let $f$ be a random completely multiplicative function, where for each prime $p$ we independently choose $f(p)\in \{-1,1\}$ uniformly at...
 - [#1145](https://erdosproblems.com/1145) — OPEN | additive combinatorics, additive basis — edited: 08 February 2026 — Let $A=\{1\leq a_1<a_2<\cdots\}$ and $B=\{1\leq b_1<b_2<\cdots\}$ be sets of integers with $a_n/b_n\to 1$. If $A+B$ contains all sufficie...
 - [#1146](https://erdosproblems.com/1146) — OPEN | number theory — edited: 23 January 2026 — We say that $A\subset \mathbb{N}$ is an essential component if $d_s(A+B)>d_s(B)$ for every $B\subset \mathbb{N}$ with $0<d_s(B)<1$ where...
-- [#1148](https://erdosproblems.com/1148) — OPEN | number theory — edited: 26 January 2026 — Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\max(x^2,y^2,z^2)\leq n$?
 - [#1150](https://erdosproblems.com/1150) — OPEN | analysis, polynomials — edited: 23 January 2026 — Does there exist a constant $c>0$ such that, for all large $n$ and all polynomials $P$ of degree $n$ with coefficients $\pm 1$,\[\max_{\l...
 - [#1151](https://erdosproblems.com/1151) — OPEN | analysis, polynomials — edited: 23 January 2026 — Given $a_1,\ldots,a_n\in [-1,1]$ let\[\mathcal{L}^nf(x) = \sum_{1\leq i\leq n}f(a_i)\ell_i(x)\]be the unique polynomial of degree $n-1$ w...
 - [#1152](https://erdosproblems.com/1152) — OPEN | analysis, polynomials — edited: 23 January 2026 — For $n\geq 1$ fix some sequence of $n$ distinct numbers $x_{1n},\ldots,x_{nn}\in [-1,1]$. Let $\epsilon=\epsilon(n)\to 0$. Does there alw...
@@ -690,8 +684,11 @@
 - [#1171](https://erdosproblems.com/1171) — OPEN | set theory, ramsey theory — edited: 26 January 2026 — Is it true that, for all finite $k<\omega$,\[\omega_1^2\to (\omega_1\omega, 3,\ldots,3)_{k+1}^2?\]
 - [#1172](https://erdosproblems.com/1172) — OPEN | set theory, ramsey theory — edited: 23 January 2026 — Establish whether the following are true assuming the generalised continuum hypothesis:\[\omega_3 \to (\omega_2,\omega_1+2)^2,\]\[\omega_...
 - [#1173](https://erdosproblems.com/1173) — OPEN | set theory, combinatorics — edited: 25 January 2026 — Assume the generalised continuum hypothesis. Let\[f: \omega_{\omega+1}\to [\omega_{\omega+1}]^{\leq \aleph_\omega}\]be a set mapping such...
-- [#1174](https://erdosproblems.com/1174) — OPEN | set theory, ramsey theory — Does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_...
+- [#1174](https://erdosproblems.com/1174) — NOT DISPROVABLE | set theory, ramsey theory — Does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_...
 - [#1175](https://erdosproblems.com/1175) — OPEN | set theory, chromatic number — Let $\kappa$ be an uncountable cardinal. Must there exist a cardinal $\lambda$ such that every graph with chromatic number $\lambda$ cont...
-- [#1176](https://erdosproblems.com/1176) — OPEN | set theory, ramsey theory — edited: 24 January 2026 — Let $G$ be a graph with chromatic number $\aleph_1$. Is it true that there is a colouring of the edges with $\aleph_1$ many colours such...
+- [#1176](https://erdosproblems.com/1176) — NOT DISPROVABLE | set theory, ramsey theory — edited: 24 January 2026 — Let $G$ be a graph with chromatic number $\aleph_1$. Is it true that there is a colouring of the edges with $\aleph_1$ many colours such...
 - [#1177](https://erdosproblems.com/1177) — OPEN | set theory, chromatic number, hypergraphs — edited: 23 January 2026 — Let $G$ be a finite $3$-uniform hypergraph, and let $F_G(\kappa)$ denote the collection of $3$-uniform hypergraphs with chromatic number...
 - [#1178](https://erdosproblems.com/1178) — OPEN | graph theory, hypergraphs — edited: 26 January 2026 — For $r\geq 3$ let $d_r(e)$ be the minimal $d$ such that\[\mathrm{ex}_r(n,\mathcal{F})=o(n^2),\]where $\mathcal{F}$ is the family of $r$-u...
+- [#1181](https://erdosproblems.com/1181) — OPEN | number theory — edited: 07 March 2026 — Let $q(n,k)$ denote the least prime which does not divide $\prod_{1\leq i\leq k}(n+i)$. Is it true that there exists some $c>0$ such that...
+- [#1182](https://erdosproblems.com/1182) — OPEN | graph theory, ramsey theory — Let $f(n)$ be maximal such that there is a connected graph $G$ with $n$ vertices and $f(n)$ edges such that\[R(K_3,G)= 2n-1.\]Let $F(n)$...
+- [#1183](https://erdosproblems.com/1183) — OPEN | combinatorics, ramsey theory — Let $f(n)$ be maximal such that in any $2$-colouring of the subsets of $\{1,\ldots,n\}$ there is always a monochromatic family of at leas...
diff --git a/packs/erdos-open-problems/data/erdos_problems.active.json b/packs/erdos-open-problems/data/erdos_problems.active.json
index 647b433..24f0c1e 100644
--- a/packs/erdos-open-problems/data/erdos_problems.active.json
+++ b/packs/erdos-open-problems/data/erdos_problems.active.json
@@ -2,30 +2,32 @@
   "schema_version": "1.0.0",
   "subset": "active",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-04-01T06:51:20Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "870c67de08d4d2a7667ad4a3cd9b930d3a9809cca047a50fa20ab5b2b22fc23d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "495 solved out of 1183 shown",
+      "solved": 495,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 691,
-    "open": 691,
+    "total": 688,
+    "open": 688,
     "closed": 0,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 2,
+      "DISPROVED": 1,
       "DISPROVED (LEAN)": 1,
-      "FALSIFIABLE": 29,
-      "NOT DISPROVABLE": 2,
+      "FALSIFIABLE": 27,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 3,
-      "OPEN": 645,
-      "PROVED": 2,
+      "OPEN": 639,
+      "PROVED": 3,
+      "PROVED (LEAN)": 1,
       "VERIFIABLE": 7
     }
   },
@@ -104,7 +106,6 @@
     122,
     123,
     124,
-    125,
     126,
     128,
     129,
@@ -295,7 +296,6 @@
     454,
     455,
     456,
-    457,
     458,
     460,
     461,
@@ -405,7 +405,6 @@
     643,
     644,
     647,
-    650,
     653,
     654,
     655,
@@ -542,7 +541,6 @@
     879,
     881,
     883,
-    884,
     885,
     886,
     887,
@@ -612,7 +610,6 @@
     993,
     995,
     996,
-    997,
     1002,
     1003,
     1004,
@@ -695,7 +692,6 @@
     1144,
     1145,
     1146,
-    1148,
     1150,
     1151,
     1152,
@@ -720,7 +716,10 @@
     1175,
     1176,
     1177,
-    1178
+    1178,
+    1181,
+    1182,
+    1183
   ],
   "problems": [
     {
@@ -870,8 +869,8 @@
       "problem_url": "/11",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Is every large odd integer $n$ the sum of a squarefree number and a power of 2?",
       "tags": [
@@ -993,8 +992,8 @@
       ],
       "last_edited": "20 January 2026",
       "latex_path": "/latex/18",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/18.lean",
       "oeis_urls": [
         "https://oeis.org/A005153"
       ],
@@ -1013,7 +1012,7 @@
       "tags": [
         "combinatorics"
       ],
-      "last_edited": "25 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/20",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/20.lean",
@@ -1063,7 +1062,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/25.lean",
       "oeis_urls": [],
       "comments_problem_id": 25,
-      "comments_count": 2
+      "comments_count": 7
     },
     {
       "problem_id": 28,
@@ -1152,7 +1151,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/33.lean",
       "oeis_urls": [],
       "comments_problem_id": 33,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 36,
@@ -1346,8 +1345,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/50",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/50.lean",
       "oeis_urls": [],
       "comments_problem_id": 50,
       "comments_count": 0
@@ -1388,7 +1387,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/52",
       "formalized": false,
       "formalized_url": "",
@@ -1747,8 +1746,8 @@
       "problem_url": "/85",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $n\\geq 4$ and $f(n)$ be minimal such that every graph on $n$ vertices with minimal degree $\\geq f(n)$ contains a $C_4$. Is it true that, for all large $n$, $f(n+1)\\geq f(n)$?",
       "tags": [
@@ -1878,7 +1877,7 @@
         "https://oeis.org/A186704"
       ],
       "comments_problem_id": 91,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 92,
@@ -2105,7 +2104,7 @@
       "tags": [
         "geometry"
       ],
-      "last_edited": "",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/106",
       "formalized": false,
       "formalized_url": "",
@@ -2206,8 +2205,8 @@
       "problem_url": "/114",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "$250",
       "statement": "If $p(z)\\in\\mathbb{C}[z]$ is a monic polynomial of degree $n$ then is the length of the curve $\\{ z\\in \\mathbb{C} : \\lvert p(z)\\rvert=1\\}$ maximised when $p(z)=z^n-1$?",
       "tags": [
@@ -2220,7 +2219,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 114,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 117,
@@ -2281,7 +2280,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/120.lean",
       "oeis_urls": [],
       "comments_problem_id": 120,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 122,
@@ -2301,7 +2300,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 122,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 123,
@@ -2345,29 +2344,6 @@
       "comments_problem_id": 124,
       "comments_count": 13
     },
-    {
-      "problem_id": 125,
-      "problem_url": "/125",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Let $A = \\{ \\sum\\epsilon_k3^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $3$, and $B=\\{ \\sum\\epsilon_k4^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $4$. Does $A+B$ have positive density?",
-      "tags": [
-        "number theory",
-        "base representations"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/125",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/125.lean",
-      "oeis_urls": [
-        "https://oeis.org/A367090"
-      ],
-      "comments_problem_id": 125,
-      "comments_count": 13
-    },
     {
       "problem_id": 126,
       "problem_url": "/126",
@@ -2826,13 +2802,13 @@
       "status_dom_id": "open",
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "There exists some constant $c>0$ such that $$R(C_4,K_n) \\ll n^{2-c}.$$",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/159",
       "formalized": false,
       "formalized_url": "",
@@ -2919,7 +2895,7 @@
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/165",
       "formalized": false,
       "formalized_url": "",
@@ -2961,7 +2937,7 @@
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "24 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/168",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/168.lean",
@@ -3102,7 +3078,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 176,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 177,
@@ -3205,11 +3181,11 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/184",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/184.lean",
       "oeis_urls": [],
       "comments_problem_id": 184,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 187,
@@ -3289,8 +3265,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/193",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/193.lean",
       "oeis_urls": [
         "https://oeis.org/A231255"
       ],
@@ -3693,7 +3669,7 @@
         "https://oeis.org/A387704"
       ],
       "comments_problem_id": 241,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 242,
@@ -3744,7 +3720,7 @@
         "https://oeis.org/A000058"
       ],
       "comments_problem_id": 243,
-      "comments_count": 6
+      "comments_count": 7
     },
     {
       "problem_id": 244,
@@ -3872,8 +3848,8 @@
       ],
       "last_edited": "07 December 2025",
       "latex_path": "/latex/254",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/254.lean",
       "oeis_urls": [],
       "comments_problem_id": 254,
       "comments_count": 3
@@ -3952,8 +3928,8 @@
       ],
       "last_edited": "01 February 2026",
       "latex_path": "/latex/260",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/260.lean",
       "oeis_urls": [],
       "comments_problem_id": 260,
       "comments_count": 2
@@ -4162,7 +4138,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/274.lean",
       "oeis_urls": [],
       "comments_problem_id": 274,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 276,
@@ -4270,7 +4246,7 @@
         "https://oeis.org/A380791"
       ],
       "comments_problem_id": 283,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 287,
@@ -4723,8 +4699,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/323",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/323.lean",
       "oeis_urls": [],
       "comments_problem_id": 323,
       "comments_count": 0
@@ -4769,7 +4745,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/325.lean",
       "oeis_urls": [],
       "comments_problem_id": 325,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 326,
@@ -4790,7 +4766,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/326.lean",
       "oeis_urls": [],
       "comments_problem_id": 326,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 327,
@@ -4849,7 +4825,7 @@
         "number theory",
         "additive basis"
       ],
-      "last_edited": "08 December 2025",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/330",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/330.lean",
@@ -4893,7 +4869,10 @@
       "latex_path": "/latex/334",
       "formalized": false,
       "formalized_url": "",
-      "oeis_urls": [],
+      "oeis_urls": [
+        "https://oeis.org/A045535",
+        "https://oeis.org/A062241"
+      ],
       "comments_problem_id": 334,
       "comments_count": 2
     },
@@ -5019,13 +4998,13 @@
       ],
       "last_edited": "30 September 2025",
       "latex_path": "/latex/342",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/342.lean",
       "oeis_urls": [
         "https://oeis.org/A002858"
       ],
       "comments_problem_id": 342,
-      "comments_count": 11
+      "comments_count": 18
     },
     {
       "problem_id": 345,
@@ -5111,7 +5090,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/349.lean",
       "oeis_urls": [],
       "comments_problem_id": 349,
-      "comments_count": 8
+      "comments_count": 12
     },
     {
       "problem_id": 351,
@@ -5218,7 +5197,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/358.lean",
       "oeis_urls": [],
       "comments_problem_id": 358,
-      "comments_count": 19
+      "comments_count": 21
     },
     {
       "problem_id": 359,
@@ -5309,7 +5288,7 @@
         "https://oeis.org/A175155"
       ],
       "comments_problem_id": 365,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 366,
@@ -5319,12 +5298,12 @@
       "status_label": "VERIFIABLE",
       "status_detail": "Open, but could be proved with a finite example.",
       "prize_amount": "",
-      "statement": "Are there any 2-full $n$ such that $n+1$ is 3-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
+      "statement": "Are there any $2$-full $n$ such that $n+1$ is $3$-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "20 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/366",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/366.lean",
@@ -5342,12 +5321,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $B_2(n)$ be the 2-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
+      "statement": "Let $B_2(n)$ be the $2$-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "08 February 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/367",
       "formalized": false,
       "formalized_url": "",
@@ -5384,8 +5363,8 @@
       "problem_url": "/369",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $\\epsilon>0$ and $k\\geq 2$. Is it true that, for all sufficiently large $n$, there is a sequence of $k$ consecutive integers in $\\{1,\\ldots,n\\}$ all of which are $n^\\epsilon$-smooth?",
       "tags": [
@@ -5397,7 +5376,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 369,
-      "comments_count": 0
+      "comments_count": 11
     },
     {
       "problem_id": 371,
@@ -5467,7 +5446,7 @@
         "https://oeis.org/A389148"
       ],
       "comments_problem_id": 374,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 375,
@@ -5540,8 +5519,8 @@
       "problem_url": "/380",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED",
+      "status_detail": "This has been solved in the affirmative.",
       "prize_amount": "",
       "statement": "We call an interval $[u,v]$ 'bad' if the greatest prime factor of $\\prod_{u\\leq m\\leq v}m$ occurs with an exponent greater than $1$. Let $B(x)$ count the number of $n\\leq x$ which are contained in at least one bad interval. Is it true that\\[B(x)\\sim \\#\\{ n\\leq x: P(n)^2\\mid n\\},\\]where $P(n)$ is the largest prime factor of $n$?",
       "tags": [
@@ -5558,7 +5537,7 @@
         "https://oeis.org/A389100"
       ],
       "comments_problem_id": 380,
-      "comments_count": 5
+      "comments_count": 9
     },
     {
       "problem_id": 382,
@@ -5645,7 +5624,7 @@
         "https://oeis.org/A280992"
       ],
       "comments_problem_id": 386,
-      "comments_count": 12
+      "comments_count": 13
     },
     {
       "problem_id": 387,
@@ -5686,7 +5665,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -5708,7 +5687,7 @@
         "https://oeis.org/A375071"
       ],
       "comments_problem_id": 389,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 390,
@@ -5799,7 +5778,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 30
     },
     {
       "problem_id": 398,
@@ -5814,15 +5793,16 @@
         "number theory",
         "factorials"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/398",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/398.lean",
       "oeis_urls": [
+        "https://oeis.org/A141399",
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 9
     },
     {
       "problem_id": 400,
@@ -5839,8 +5819,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/400",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/400.lean",
       "oeis_urls": [],
       "comments_problem_id": 400,
       "comments_count": 0
@@ -6192,7 +6172,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -6200,7 +6180,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -6214,7 +6194,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/424",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/424.lean",
@@ -6363,8 +6343,8 @@
       ],
       "last_edited": "27 December 2025",
       "latex_path": "/latex/445",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/445.lean",
       "oeis_urls": [],
       "comments_problem_id": 445,
       "comments_count": 1
@@ -6496,28 +6476,6 @@
       "comments_problem_id": 456,
       "comments_count": 2
     },
-    {
-      "problem_id": 457,
-      "problem_url": "/457",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Is there some $\\epsilon>0$ such that there are infinitely many $n$ where all primes $p\\leq (2+\\epsilon)\\log n$ divide\\[\\prod_{1\\leq i\\leq \\log n}(n+i)?\\]",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "07 October 2025",
-      "latex_path": "/latex/457",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/457.lean",
-      "oeis_urls": [
-        "https://oeis.org/A391668"
-      ],
-      "comments_problem_id": 457,
-      "comments_count": 7
-    },
     {
       "problem_id": 458,
       "problem_url": "/458",
@@ -6775,7 +6733,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -6904,8 +6862,8 @@
       "problem_url": "/488",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "",
       "statement": "Let $A$ be a finite set and\\[B=\\{ n \\geq 1 : a\\mid n\\textrm{ for some }a\\in A\\}.\\]Is it true that, for every $m>n\\geq \\max(A)$,\\[\\frac{\\lvert B\\cap [1,m]\\rvert }{m}< 2\\frac{\\lvert B\\cap [1,n]\\rvert}{n}?\\]",
       "tags": [
@@ -6917,7 +6875,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/488.lean",
       "oeis_urls": [],
       "comments_problem_id": 488,
-      "comments_count": 14
+      "comments_count": 27
     },
     {
       "problem_id": 489,
@@ -7168,7 +7126,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/517.lean",
       "oeis_urls": [],
       "comments_problem_id": 517,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 520,
@@ -7478,12 +7436,12 @@
       "status_dom_id": "open",
       "status_label": "FALSIFIABLE",
       "status_detail": "Open, but could be disproved with a finite counterexample.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "Let $n\\geq k+1$. Every graph on $n$ vertices with at least $\\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.",
       "tags": [
         "graph theory"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/548",
       "formalized": false,
       "formalized_url": "",
@@ -7809,7 +7767,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 569,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 571,
@@ -7824,7 +7782,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -7882,8 +7840,8 @@
       "problem_url": "/574",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "DISPROVED",
+      "status_detail": "This has been solved in the negative.",
       "prize_amount": "",
       "statement": "Is it true that, for $k\\geq 2$,\\[\\mathrm{ex}(n;\\{C_{2k-1},C_{2k}\\})=(1+o(1))(n/2)^{1+\\frac{1}{k}}.\\]",
       "tags": [
@@ -7896,7 +7854,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 574,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 575,
@@ -7999,7 +7957,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -8211,7 +8169,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/598.lean",
       "oeis_urls": [],
       "comments_problem_id": 598,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 600,
@@ -8309,7 +8267,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -8456,7 +8414,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/617.lean",
       "oeis_urls": [],
       "comments_problem_id": 617,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 619,
@@ -8662,7 +8620,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -8831,26 +8789,6 @@
       "comments_problem_id": 647,
       "comments_count": 6
     },
-    {
-      "problem_id": 650,
-      "problem_url": "/650",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Let $f(m)$ be such that if $A\\subseteq \\{1,\\ldots,N\\}$ has $\\lvert A\\rvert=m$ then every interval in $[1,\\infty)$ of length $2N$ contains $\\geq f(m)$ many distinct integers $b_1,\\ldots,b_r$ where each $b_i$ is divisible by some $a_i\\in A$, where $a_1,\\ldots,a_r$ are distinct. Estimate $f(m)$. In particular is it true that $f(m)\\ll m^{1/2}$?",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/650",
-      "formalized": false,
-      "formalized_url": "",
-      "oeis_urls": [],
-      "comments_problem_id": 650,
-      "comments_count": 0
-    },
     {
       "problem_id": 653,
       "problem_url": "/653",
@@ -9228,7 +9166,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/677.lean",
       "oeis_urls": [],
       "comments_problem_id": 677,
-      "comments_count": 0
+      "comments_count": 7
     },
     {
       "problem_id": 679,
@@ -9310,8 +9248,8 @@
       ],
       "last_edited": "31 December 2025",
       "latex_path": "/latex/683",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/683.lean",
       "oeis_urls": [
         "https://oeis.org/A006530",
         "https://oeis.org/A074399",
@@ -9334,7 +9272,7 @@
         "primes",
         "binomial coefficients"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/684",
       "formalized": false,
       "formalized_url": "",
@@ -9384,7 +9322,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/686.lean",
       "oeis_urls": [],
       "comments_problem_id": 686,
-      "comments_count": 16
+      "comments_count": 37
     },
     {
       "problem_id": 687,
@@ -9660,7 +9598,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 706,
@@ -9715,13 +9653,13 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/709",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 709,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 710,
@@ -9800,7 +9738,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "06 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/713",
       "formalized": false,
       "formalized_url": "",
@@ -10118,17 +10056,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
+      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive (upper) density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive (upper) density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/741",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/741.lean",
       "oeis_urls": [],
       "comments_problem_id": 741,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 743,
@@ -10711,7 +10649,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -10770,8 +10708,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/812",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/812.lean",
       "oeis_urls": [],
       "comments_problem_id": 812,
       "comments_count": 0
@@ -11041,7 +10979,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/835.lean",
       "oeis_urls": [],
       "comments_problem_id": 835,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 836,
@@ -11287,7 +11225,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -11317,8 +11255,8 @@
       "problem_url": "/855",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "If $\\pi(x)$ counts the number of primes in $[1,x]$ then is it true that (for large $x$ and $y$)\\[\\pi(x+y) \\leq \\pi(x)+\\pi(y)?\\]",
       "tags": [
@@ -11738,27 +11676,6 @@
       "comments_problem_id": 883,
       "comments_count": 3
     },
-    {
-      "problem_id": 884,
-      "problem_url": "/884",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Is it true that, for any $n$, if $d_1<\\cdots <d_t$ are the divisors of $n$, then\\[\\sum_{1\\leq i<j\\leq t}\\frac{1}{d_j-d_i} \\ll 1+\\sum_{1\\leq i<t}\\frac{1}{d_{i+1}-d_i},\\]where the implied constant is absolute?",
-      "tags": [
-        "number theory",
-        "divisors"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/884",
-      "formalized": false,
-      "formalized_url": "",
-      "oeis_urls": [],
-      "comments_problem_id": 884,
-      "comments_count": 5
-    },
     {
       "problem_id": 885,
       "problem_url": "/885",
@@ -12264,7 +12181,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/931.lean",
       "oeis_urls": [],
       "comments_problem_id": 931,
-      "comments_count": 0
+      "comments_count": 4
     },
     {
       "problem_id": 932,
@@ -12326,7 +12243,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -12480,7 +12397,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/943.lean",
       "oeis_urls": [],
       "comments_problem_id": 943,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 944,
@@ -12830,7 +12747,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/968",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/968.lean",
@@ -12944,7 +12861,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 975,
@@ -12998,17 +12915,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$ then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
+      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$, and for all primes $p$ there exists $n$ such that $p^{k-2}\\nmid f(n)$, then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "05 March 2026",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/978",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/978.lean",
       "oeis_urls": [],
       "comments_problem_id": 978,
-      "comments_count": 8
+      "comments_count": 16
     },
     {
       "problem_id": 979,
@@ -13098,7 +13015,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -13183,7 +13100,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 995,
@@ -13226,28 +13143,6 @@
       "comments_problem_id": 996,
       "comments_count": 0
     },
-    {
-      "problem_id": 997,
-      "problem_url": "/997",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Call $x_1,x_2,\\ldots \\in (0,1)$ well-distributed if, for every $\\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\\subseteq [0,1]$,\\[\\lvert \\# \\{ n<m\\leq n+k : x_m\\in I\\} - \\lvert I\\rvert k\\rvert < \\epsilon k.\\]Is it true that, for every $\\alpha$, the sequence $\\{ \\alpha p_n\\}$ is not well-distributed, if $p_n$ is the sequence of primes?",
-      "tags": [
-        "analysis",
-        "discrepancy",
-        "primes"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/997",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/997.lean",
-      "oeis_urls": [],
-      "comments_problem_id": 997,
-      "comments_count": 0
-    },
     {
       "problem_id": 1002,
       "problem_url": "/1002",
@@ -13490,12 +13385,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "If $R(k,l)$ is the Ramsey number then prove the existence of some $c>0$ such that\\[\\lim_k \\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
+      "statement": "Let $R(k,l)$ be the usual Ramsey number: the smallest $n$ such that if the edges of $K_n$ are coloured red and blue then there exists either a red $K_k$ or a blue $K_l$. Prove the existence of some $c>0$ such that\\[\\lim_{k\\to \\infty}\\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "03 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/1030",
       "formalized": false,
       "formalized_url": "",
@@ -13504,7 +13399,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1032,
@@ -13585,7 +13480,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1038.lean",
       "oeis_urls": [],
       "comments_problem_id": 1038,
-      "comments_count": 127
+      "comments_count": 134
     },
     {
       "problem_id": 1039,
@@ -13606,7 +13501,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -13626,7 +13521,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -13647,15 +13542,15 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1041.lean",
       "oeis_urls": [],
       "comments_problem_id": 1041,
-      "comments_count": 2
+      "comments_count": 41
     },
     {
       "problem_id": 1045,
       "problem_url": "/1045",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $z_1,\\ldots,z_n\\in \\mathbb{C}$ with $\\lvert z_i-z_j\\rvert\\leq 2$ for all $i,j$, and\\[\\Delta(z_1,\\ldots,z_n)=\\prod_{i\\neq j}\\lvert z_i-z_j\\rvert.\\]What is the maximum possible value of $\\Delta$? Is it maximised by taking the $z_i$ to be the vertices of a regular polygon?",
       "tags": [
@@ -13667,7 +13562,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1049,
@@ -13687,7 +13582,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1049.lean",
       "oeis_urls": [],
       "comments_problem_id": 1049,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 1052,
@@ -14087,7 +13982,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -14362,7 +14257,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -14403,7 +14298,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1097.lean",
       "oeis_urls": [],
       "comments_problem_id": 1097,
-      "comments_count": 11
+      "comments_count": 17
     },
     {
       "problem_id": 1100,
@@ -14468,7 +14363,7 @@
         "https://oeis.org/A392164"
       ],
       "comments_problem_id": 1103,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 1104,
@@ -14605,7 +14500,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -14728,7 +14623,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1131,
@@ -14770,7 +14665,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -14904,7 +14799,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -14919,7 +14814,7 @@
         "number theory",
         "primes"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1142",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1142.lean",
@@ -14927,7 +14822,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -15012,29 +14907,6 @@
       "comments_problem_id": 1146,
       "comments_count": 0
     },
-    {
-      "problem_id": 1148,
-      "problem_url": "/1148",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\\max(x^2,y^2,z^2)\\leq n$?",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "26 January 2026",
-      "latex_path": "/latex/1148",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1148.lean",
-      "oeis_urls": [
-        "https://oeis.org/A390380",
-        "https://oeis.org/A393168"
-      ],
-      "comments_problem_id": 1148,
-      "comments_count": 6
-    },
     {
       "problem_id": 1150,
       "problem_url": "/1150",
@@ -15117,7 +14989,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -15456,8 +15328,8 @@
       "problem_url": "/1174",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_3$? Does there exist a graph $G$ with no $K_{\\aleph_1}$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_{\\aleph_0}$?",
       "tags": [
@@ -15470,7 +15342,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -15498,8 +15370,8 @@
       "problem_url": "/1176",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Let $G$ be a graph with chromatic number $\\aleph_1$. Is it true that there is a colouring of the edges with $\\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?",
       "tags": [
@@ -15512,7 +15384,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1176.lean",
       "oeis_urls": [],
       "comments_problem_id": 1176,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1177,
@@ -15556,6 +15428,68 @@
       "oeis_urls": [],
       "comments_problem_id": 1178,
       "comments_count": 1
+    },
+    {
+      "problem_id": 1181,
+      "problem_url": "/1181",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $q(n,k)$ denote the least prime which does not divide $\\prod_{1\\leq i\\leq k}(n+i)$. Is it true that there exists some $c>0$ such that, for all large $n$,\\[q(n,\\log n)<(1-c)(\\log n)^2?\\]",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "07 March 2026",
+      "latex_path": "/latex/1181",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1181,
+      "comments_count": 0
+    },
+    {
+      "problem_id": 1182,
+      "problem_url": "/1182",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that there is a connected graph $G$ with $n$ vertices and $f(n)$ edges such that\\[R(K_3,G)= 2n-1.\\]Let $F(n)$ be maximal such that every connected graph $G$ with $n$ vertices and $\\leq F(n)$ edges has\\[R(K_3,G)= 2n-1.\\]Estimate $f(n)$ and $F(n)$. In particular, is it true that $F(n)/n\\to \\infty$?",
+      "tags": [
+        "graph theory",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1182",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1182,
+      "comments_count": 3
+    },
+    {
+      "problem_id": 1183,
+      "problem_url": "/1183",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that in any $2$-colouring of the subsets of $\\{1,\\ldots,n\\}$ there is always a monochromatic family of at least $f(n)$ sets which is closed under taking unions and intersections. Estimate $f(n)$. Let $F(n)$ be defined similarly, except that we only require the family be closed under taking unions. Estimate $F(n)$. In particular, is it true that $F(n)\\geq n^{\\omega(n)}$ for some $\\omega(n)\\to \\infty$ as $n\\to \\infty$, and $F(n)<(1+o(1))^n$?",
+      "tags": [
+        "combinatorics",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1183",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1183,
+      "comments_count": 10
     }
   ]
 }
diff --git a/packs/erdos-open-problems/data/erdos_problems.all.json b/packs/erdos-open-problems/data/erdos_problems.all.json
index 2570e3c..5cd682e 100644
--- a/packs/erdos-open-problems/data/erdos_problems.all.json
+++ b/packs/erdos-open-problems/data/erdos_problems.all.json
@@ -2,35 +2,35 @@
   "schema_version": "1.0.0",
   "subset": "all",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-04-01T06:51:20Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "870c67de08d4d2a7667ad4a3cd9b930d3a9809cca047a50fa20ab5b2b22fc23d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "495 solved out of 1183 shown",
+      "solved": 495,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 1179,
-    "open": 691,
-    "closed": 488,
+    "total": 1183,
+    "open": 688,
+    "closed": 495,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 9,
       "DISPROVED": 76,
-      "DISPROVED (LEAN)": 40,
-      "FALSIFIABLE": 29,
+      "DISPROVED (LEAN)": 43,
+      "FALSIFIABLE": 27,
       "INDEPENDENT": 3,
-      "NOT DISPROVABLE": 2,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 4,
-      "OPEN": 645,
-      "PROVED": 239,
-      "PROVED (LEAN)": 63,
-      "SOLVED": 52,
-      "SOLVED (LEAN)": 10,
+      "OPEN": 640,
+      "PROVED": 238,
+      "PROVED (LEAN)": 70,
+      "SOLVED": 51,
+      "SOLVED (LEAN)": 11,
       "VERIFIABLE": 7
     }
   },
@@ -1213,7 +1213,11 @@
     1176,
     1177,
     1178,
-    1179
+    1179,
+    1180,
+    1181,
+    1182,
+    1183
   ],
   "problems": [
     {
@@ -1453,8 +1457,8 @@
       "problem_url": "/11",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Is every large odd integer $n$ the sum of a squarefree number and a power of 2?",
       "tags": [
@@ -1622,8 +1626,8 @@
       ],
       "last_edited": "20 January 2026",
       "latex_path": "/latex/18",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/18.lean",
       "oeis_urls": [
         "https://oeis.org/A005153"
       ],
@@ -1643,7 +1647,7 @@
         "graph theory",
         "chromatic number"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/19",
       "formalized": false,
       "formalized_url": "",
@@ -1663,7 +1667,7 @@
       "tags": [
         "combinatorics"
       ],
-      "last_edited": "25 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/20",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/20.lean",
@@ -1776,7 +1780,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/25.lean",
       "oeis_urls": [],
       "comments_problem_id": 25,
-      "comments_count": 2
+      "comments_count": 7
     },
     {
       "problem_id": 26,
@@ -1949,7 +1953,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/33.lean",
       "oeis_urls": [],
       "comments_problem_id": 33,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 34,
@@ -2318,8 +2322,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/50",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/50.lean",
       "oeis_urls": [],
       "comments_problem_id": 50,
       "comments_count": 0
@@ -2360,7 +2364,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/52",
       "formalized": false,
       "formalized_url": "",
@@ -3065,8 +3069,8 @@
       "problem_url": "/85",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $n\\geq 4$ and $f(n)$ be minimal such that every graph on $n$ vertices with minimal degree $\\geq f(n)$ contains a $C_4$. Is it true that, for all large $n$, $f(n+1)\\geq f(n)$?",
       "tags": [
@@ -3217,7 +3221,7 @@
         "https://oeis.org/A186704"
       ],
       "comments_problem_id": 91,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 92,
@@ -3532,7 +3536,7 @@
       "tags": [
         "geometry"
       ],
-      "last_edited": "",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/106",
       "formalized": false,
       "formalized_url": "",
@@ -3696,8 +3700,8 @@
       "problem_url": "/114",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "$250",
       "statement": "If $p(z)\\in\\mathbb{C}[z]$ is a monic polynomial of degree $n$ then is the length of the curve $\\{ z\\in \\mathbb{C} : \\lvert p(z)\\rvert=1\\}$ maximised when $p(z)=z^n-1$?",
       "tags": [
@@ -3710,7 +3714,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 114,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 115,
@@ -3834,7 +3838,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/120.lean",
       "oeis_urls": [],
       "comments_problem_id": 120,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 121,
@@ -3884,7 +3888,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 122,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 123,
@@ -3931,17 +3935,17 @@
     {
       "problem_id": 125,
       "problem_url": "/125",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
       "prize_amount": "",
-      "statement": "Let $A = \\{ \\sum\\epsilon_k3^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $3$, and $B=\\{ \\sum\\epsilon_k4^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $4$. Does $A+B$ have positive density?",
+      "statement": "Let $A = \\{ \\sum\\epsilon_k3^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $3$, and $B=\\{ \\sum\\epsilon_k4^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $4$. Does $A+B$ have positive lower density?",
       "tags": [
         "number theory",
         "base representations"
       ],
-      "last_edited": "",
+      "last_edited": "30 March 2026",
       "latex_path": "/latex/125",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/125.lean",
@@ -3949,7 +3953,7 @@
         "https://oeis.org/A367090"
       ],
       "comments_problem_id": 125,
-      "comments_count": 13
+      "comments_count": 21
     },
     {
       "problem_id": 126,
@@ -4474,8 +4478,8 @@
       "problem_url": "/150",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let $c(n)$ be the maximum number of minimal cuts a graph on $n$ vertices can have. Does $c(n)^{1/n}\\to \\alpha$ for some $\\alpha <2$?",
       "tags": [
@@ -4487,7 +4491,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 150,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 151,
@@ -4663,13 +4667,13 @@
       "status_dom_id": "open",
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "There exists some constant $c>0$ such that $$R(C_4,K_n) \\ll n^{2-c}.$$",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/159",
       "formalized": false,
       "formalized_url": "",
@@ -4800,7 +4804,7 @@
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/165",
       "formalized": false,
       "formalized_url": "",
@@ -4865,7 +4869,7 @@
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "24 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/168",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/168.lean",
@@ -5050,7 +5054,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 176,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 177,
@@ -5163,12 +5167,12 @@
       "status_dom_id": "solved",
       "status_label": "PROVED",
       "status_detail": "This has been solved in the affirmative.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "Let $k\\geq 3$. What is the maximum number of edges that a graph on $n$ vertices can contain if it does not have a $k$-regular subgraph? Is it $\\ll n^{1+o(1)}$?",
       "tags": [
         "graph theory"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/182",
       "formalized": false,
       "formalized_url": "",
@@ -5214,11 +5218,11 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/184",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/184.lean",
       "oeis_urls": [],
       "comments_problem_id": 184,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 185,
@@ -5405,8 +5409,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/193",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/193.lean",
       "oeis_urls": [
         "https://oeis.org/A231255"
       ],
@@ -5632,8 +5636,8 @@
       "problem_url": "/204",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "DISPROVED",
-      "status_detail": "This has been solved in the negative.",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Are there $n$ such that there is a covering system with moduli the divisors of $n$ which is 'as disjoint as possible'? That is, for all $d\\mid n$ with $d>1$ there is an associated $a_d$ such that every integer is congruent to some $a_d\\pmod{d}$, and if there is some integer $x$ with\\[x\\equiv a_d\\pmod{d}\\textrm{ and }x\\equiv a_{d'}\\pmod{d'}\\]then $(d,d')=1$.",
       "tags": [
@@ -5646,7 +5650,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/204.lean",
       "oeis_urls": [],
       "comments_problem_id": 204,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 205,
@@ -6015,7 +6019,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 221,
-      "comments_count": 2
+      "comments_count": 4
     },
     {
       "problem_id": 222,
@@ -6093,7 +6097,7 @@
       "tags": [
         "analysis"
       ],
-      "last_edited": "01 February 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/225",
       "formalized": false,
       "formalized_url": "",
@@ -6437,7 +6441,7 @@
         "https://oeis.org/A387704"
       ],
       "comments_problem_id": 241,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 242,
@@ -6488,7 +6492,7 @@
         "https://oeis.org/A000058"
       ],
       "comments_problem_id": 243,
-      "comments_count": 6
+      "comments_count": 7
     },
     {
       "problem_id": 244,
@@ -6719,8 +6723,8 @@
       ],
       "last_edited": "07 December 2025",
       "latex_path": "/latex/254",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/254.lean",
       "oeis_urls": [],
       "comments_problem_id": 254,
       "comments_count": 3
@@ -6841,8 +6845,8 @@
       ],
       "last_edited": "01 February 2026",
       "latex_path": "/latex/260",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/260.lean",
       "oeis_urls": [],
       "comments_problem_id": 260,
       "comments_count": 2
@@ -7133,7 +7137,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/274.lean",
       "oeis_urls": [],
       "comments_problem_id": 274,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 275,
@@ -7325,7 +7329,7 @@
         "https://oeis.org/A380791"
       ],
       "comments_problem_id": 283,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 284,
@@ -7642,7 +7646,7 @@
         "number theory",
         "unit fractions"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/298",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/298.lean",
@@ -7994,7 +7998,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 314,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 315,
@@ -8190,8 +8194,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/323",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/323.lean",
       "oeis_urls": [],
       "comments_problem_id": 323,
       "comments_count": 0
@@ -8236,7 +8240,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/325.lean",
       "oeis_urls": [],
       "comments_problem_id": 325,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 326,
@@ -8257,7 +8261,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/326.lean",
       "oeis_urls": [],
       "comments_problem_id": 326,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 327,
@@ -8337,7 +8341,7 @@
         "number theory",
         "additive basis"
       ],
-      "last_edited": "08 December 2025",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/330",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/330.lean",
@@ -8423,7 +8427,10 @@
       "latex_path": "/latex/334",
       "formalized": false,
       "formalized_url": "",
-      "oeis_urls": [],
+      "oeis_urls": [
+        "https://oeis.org/A045535",
+        "https://oeis.org/A062241"
+      ],
       "comments_problem_id": 334,
       "comments_count": 2
     },
@@ -8592,13 +8599,13 @@
       ],
       "last_edited": "30 September 2025",
       "latex_path": "/latex/342",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/342.lean",
       "oeis_urls": [
         "https://oeis.org/A002858"
       ],
       "comments_problem_id": 342,
-      "comments_count": 11
+      "comments_count": 18
     },
     {
       "problem_id": 343,
@@ -8747,7 +8754,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/349.lean",
       "oeis_urls": [],
       "comments_problem_id": 349,
-      "comments_count": 8
+      "comments_count": 12
     },
     {
       "problem_id": 350,
@@ -8871,7 +8878,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/355.lean",
       "oeis_urls": [],
       "comments_problem_id": 355,
-      "comments_count": 16
+      "comments_count": 18
     },
     {
       "problem_id": 356,
@@ -8936,7 +8943,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/358.lean",
       "oeis_urls": [],
       "comments_problem_id": 358,
-      "comments_count": 19
+      "comments_count": 21
     },
     {
       "problem_id": 359,
@@ -9025,8 +9032,8 @@
       "problem_url": "/363",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "DISPROVED",
-      "status_detail": "This has been solved in the negative.",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Is it true that there are only finitely many collections of disjoint intervals $I_1,\\ldots,I_n$ of size $\\lvert I_i\\rvert \\geq 4$ for $1\\leq i\\leq n$ such that\\[\\prod_{1\\leq i\\leq n}\\prod_{m\\in I_i}m\\]is a square?",
       "tags": [
@@ -9038,7 +9045,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 363,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 364,
@@ -9087,7 +9094,7 @@
         "https://oeis.org/A175155"
       ],
       "comments_problem_id": 365,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 366,
@@ -9097,12 +9104,12 @@
       "status_label": "VERIFIABLE",
       "status_detail": "Open, but could be proved with a finite example.",
       "prize_amount": "",
-      "statement": "Are there any 2-full $n$ such that $n+1$ is 3-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
+      "statement": "Are there any $2$-full $n$ such that $n+1$ is $3$-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "20 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/366",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/366.lean",
@@ -9120,12 +9127,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $B_2(n)$ be the 2-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
+      "statement": "Let $B_2(n)$ be the $2$-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "08 February 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/367",
       "formalized": false,
       "formalized_url": "",
@@ -9162,8 +9169,8 @@
       "problem_url": "/369",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $\\epsilon>0$ and $k\\geq 2$. Is it true that, for all sufficiently large $n$, there is a sequence of $k$ consecutive integers in $\\{1,\\ldots,n\\}$ all of which are $n^\\epsilon$-smooth?",
       "tags": [
@@ -9175,7 +9182,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 369,
-      "comments_count": 0
+      "comments_count": 11
     },
     {
       "problem_id": 370,
@@ -9287,7 +9294,7 @@
         "https://oeis.org/A389148"
       ],
       "comments_problem_id": 374,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 375,
@@ -9402,8 +9409,8 @@
       "problem_url": "/380",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED",
+      "status_detail": "This has been solved in the affirmative.",
       "prize_amount": "",
       "statement": "We call an interval $[u,v]$ 'bad' if the greatest prime factor of $\\prod_{u\\leq m\\leq v}m$ occurs with an exponent greater than $1$. Let $B(x)$ count the number of $n\\leq x$ which are contained in at least one bad interval. Is it true that\\[B(x)\\sim \\#\\{ n\\leq x: P(n)^2\\mid n\\},\\]where $P(n)$ is the largest prime factor of $n$?",
       "tags": [
@@ -9420,7 +9427,7 @@
         "https://oeis.org/A389100"
       ],
       "comments_problem_id": 380,
-      "comments_count": 5
+      "comments_count": 9
     },
     {
       "problem_id": 381,
@@ -9551,7 +9558,7 @@
         "https://oeis.org/A280992"
       ],
       "comments_problem_id": 386,
-      "comments_count": 12
+      "comments_count": 13
     },
     {
       "problem_id": 387,
@@ -9592,7 +9599,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -9614,7 +9621,7 @@
         "https://oeis.org/A375071"
       ],
       "comments_problem_id": 389,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 390,
@@ -9770,7 +9777,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 30
     },
     {
       "problem_id": 397,
@@ -9806,15 +9813,16 @@
         "number theory",
         "factorials"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/398",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/398.lean",
       "oeis_urls": [
+        "https://oeis.org/A141399",
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 9
     },
     {
       "problem_id": 399,
@@ -9852,8 +9860,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/400",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/400.lean",
       "oeis_urls": [],
       "comments_problem_id": 400,
       "comments_count": 0
@@ -10354,7 +10362,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -10362,7 +10370,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -10376,7 +10384,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/424",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/424.lean",
@@ -10814,8 +10822,8 @@
       ],
       "last_edited": "27 December 2025",
       "latex_path": "/latex/445",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/445.lean",
       "oeis_urls": [],
       "comments_problem_id": 445,
       "comments_count": 1
@@ -11055,16 +11063,16 @@
     {
       "problem_id": 457,
       "problem_url": "/457",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Is there some $\\epsilon>0$ such that there are infinitely many $n$ where all primes $p\\leq (2+\\epsilon)\\log n$ divide\\[\\prod_{1\\leq i\\leq \\log n}(n+i)?\\]",
       "tags": [
         "number theory"
       ],
-      "last_edited": "07 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/457",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/457.lean",
@@ -11072,7 +11080,7 @@
         "https://oeis.org/A391668"
       ],
       "comments_problem_id": 457,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 458,
@@ -11102,8 +11110,8 @@
       "problem_url": "/459",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "SOLVED",
-      "status_detail": "This has been resolved in some other way than a proof or disproof.",
+      "status_label": "SOLVED (LEAN)",
+      "status_detail": "This has been resolved in some other way than a proof or disproof, and that resolution verified in Lean.",
       "prize_amount": "",
       "statement": "Let $f(u)$ be the largest $v$ such that no $m\\in (u,v)$ is composed entirely of primes dividing $uv$. Estimate $f(u)$.",
       "tags": [
@@ -11118,7 +11126,7 @@
         "https://oeis.org/A289280"
       ],
       "comments_problem_id": 459,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 460,
@@ -11456,7 +11464,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -11731,8 +11739,8 @@
       "problem_url": "/488",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "",
       "statement": "Let $A$ be a finite set and\\[B=\\{ n \\geq 1 : a\\mid n\\textrm{ for some }a\\in A\\}.\\]Is it true that, for every $m>n\\geq \\max(A)$,\\[\\frac{\\lvert B\\cap [1,m]\\rvert }{m}< 2\\frac{\\lvert B\\cap [1,n]\\rvert}{n}?\\]",
       "tags": [
@@ -11744,7 +11752,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/488.lean",
       "oeis_urls": [],
       "comments_problem_id": 488,
-      "comments_count": 14
+      "comments_count": 27
     },
     {
       "problem_id": 489,
@@ -11865,7 +11873,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/494.lean",
       "oeis_urls": [],
       "comments_problem_id": 494,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 495,
@@ -12343,7 +12351,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/517.lean",
       "oeis_urls": [],
       "comments_problem_id": 517,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 518,
@@ -12824,7 +12832,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/540",
       "formalized": false,
       "formalized_url": "",
@@ -12990,12 +12998,12 @@
       "status_dom_id": "open",
       "status_label": "FALSIFIABLE",
       "status_detail": "Open, but could be disproved with a finite counterexample.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "Let $n\\geq k+1$. Every graph on $n$ vertices with at least $\\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.",
       "tags": [
         "graph theory"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/548",
       "formalized": false,
       "formalized_url": "",
@@ -13451,7 +13459,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 569,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 570,
@@ -13487,7 +13495,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -13545,8 +13553,8 @@
       "problem_url": "/574",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "DISPROVED",
+      "status_detail": "This has been solved in the negative.",
       "prize_amount": "",
       "statement": "Is it true that, for $k\\geq 2$,\\[\\mathrm{ex}(n;\\{C_{2k-1},C_{2k}\\})=(1+o(1))(n/2)^{1+\\frac{1}{k}}.\\]",
       "tags": [
@@ -13559,7 +13567,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 574,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 575,
@@ -13743,7 +13751,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -14061,7 +14069,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/598.lean",
       "oeis_urls": [],
       "comments_problem_id": 598,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 599,
@@ -14180,7 +14188,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -14450,7 +14458,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/617.lean",
       "oeis_urls": [],
       "comments_problem_id": 617,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 618,
@@ -14779,7 +14787,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -15119,22 +15127,24 @@
     {
       "problem_id": 650,
       "problem_url": "/650",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
-      "statement": "Let $f(m)$ be such that if $A\\subseteq \\{1,\\ldots,N\\}$ has $\\lvert A\\rvert=m$ then every interval in $[1,\\infty)$ of length $2N$ contains $\\geq f(m)$ many distinct integers $b_1,\\ldots,b_r$ where each $b_i$ is divisible by some $a_i\\in A$, where $a_1,\\ldots,a_r$ are distinct. Estimate $f(m)$. In particular is it true that $f(m)\\ll m^{1/2}$?",
+      "statement": "Let $f(m)$ be such that if $A\\subseteq \\{1,\\ldots,N\\}$ has $\\lvert A\\rvert=m$ then every interval in $[1,\\infty)$ of length $2N$ contains $\\geq f(m)$ many distinct integers $b_1,\\ldots,b_r$ where each $b_i$ is divisible by some $a_i\\in A$, where $a_1,\\ldots,a_r$ are distinct. Estimate $f(m)$. In particular is it true that $f(m)\\leq \\sqrt{m}$?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/650",
       "formalized": false,
       "formalized_url": "",
-      "oeis_urls": [],
+      "oeis_urls": [
+        "https://oeis.org/A027434"
+      ],
       "comments_problem_id": 650,
-      "comments_count": 0
+      "comments_count": 28
     },
     {
       "problem_id": 651,
@@ -15698,7 +15708,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/677.lean",
       "oeis_urls": [],
       "comments_problem_id": 677,
-      "comments_count": 0
+      "comments_count": 7
     },
     {
       "problem_id": 678,
@@ -15823,8 +15833,8 @@
       ],
       "last_edited": "31 December 2025",
       "latex_path": "/latex/683",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/683.lean",
       "oeis_urls": [
         "https://oeis.org/A006530",
         "https://oeis.org/A074399",
@@ -15847,7 +15857,7 @@
         "primes",
         "binomial coefficients"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/684",
       "formalized": false,
       "formalized_url": "",
@@ -15897,7 +15907,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/686.lean",
       "oeis_urls": [],
       "comments_problem_id": 686,
-      "comments_count": 16
+      "comments_count": 37
     },
     {
       "problem_id": 687,
@@ -16278,7 +16288,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 705,
@@ -16375,13 +16385,13 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/709",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 709,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 710,
@@ -16460,7 +16470,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "06 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/713",
       "formalized": false,
       "formalized_url": "",
@@ -16604,7 +16614,7 @@
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "26 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/720",
       "formalized": false,
       "formalized_url": "",
@@ -16654,7 +16664,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 722,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 723,
@@ -16784,7 +16794,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/728.lean",
       "oeis_urls": [],
       "comments_problem_id": 728,
-      "comments_count": 84
+      "comments_count": 86
     },
     {
       "problem_id": 729,
@@ -17048,17 +17058,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
+      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive (upper) density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive (upper) density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/741",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/741.lean",
       "oeis_urls": [],
       "comments_problem_id": 741,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 742,
@@ -17354,8 +17364,8 @@
       "problem_url": "/756",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $A\\subset \\mathbb{R}^2$ be a set of $n$ points. Can there be $\\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$?",
       "tags": [
@@ -17368,7 +17378,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 756,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 757,
@@ -17968,20 +17978,20 @@
       "problem_url": "/785",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $A,B\\subseteq \\mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\\lvert A\\cap [1,x]\\rvert$ and similarly for $B(x)$. Is it true that if $A(x)B(x)\\sim x$ then\\[A(x)B(x)-x\\to \\infty\\]as $x\\to \\infty$?",
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/785",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 785,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 786,
@@ -18473,7 +18483,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -18532,8 +18542,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/812",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/812.lean",
       "oeis_urls": [],
       "comments_problem_id": 812,
       "comments_count": 0
@@ -19016,7 +19026,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/835.lean",
       "oeis_urls": [],
       "comments_problem_id": 835,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 836,
@@ -19285,7 +19295,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/848.lean",
       "oeis_urls": [],
       "comments_problem_id": 848,
-      "comments_count": 18
+      "comments_count": 47
     },
     {
       "problem_id": 849,
@@ -19406,7 +19416,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -19436,8 +19446,8 @@
       "problem_url": "/855",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "If $\\pi(x)$ counts the number of primes in $[1,x]$ then is it true that (for large $x$ and $y$)\\[\\pi(x+y) \\leq \\pi(x)+\\pi(y)?\\]",
       "tags": [
@@ -20054,23 +20064,23 @@
     {
       "problem_id": 884,
       "problem_url": "/884",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "DISPROVED",
+      "status_detail": "This has been solved in the negative.",
       "prize_amount": "",
       "statement": "Is it true that, for any $n$, if $d_1<\\cdots <d_t$ are the divisors of $n$, then\\[\\sum_{1\\leq i<j\\leq t}\\frac{1}{d_j-d_i} \\ll 1+\\sum_{1\\leq i<t}\\frac{1}{d_{i+1}-d_i},\\]where the implied constant is absolute?",
       "tags": [
         "number theory",
         "divisors"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/884",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 884,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 885,
@@ -20397,7 +20407,7 @@
       "tags": [
         "graph theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/900",
       "formalized": false,
       "formalized_url": "",
@@ -20694,7 +20704,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 914,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 915,
@@ -20883,7 +20893,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 923,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 924,
@@ -21047,7 +21057,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/931.lean",
       "oeis_urls": [],
       "comments_problem_id": 931,
-      "comments_count": 0
+      "comments_count": 4
     },
     {
       "problem_id": 932,
@@ -21109,7 +21119,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -21307,7 +21317,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/943.lean",
       "oeis_urls": [],
       "comments_problem_id": 943,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 944,
@@ -21828,7 +21838,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/968",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/968.lean",
@@ -21942,7 +21952,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 974,
@@ -22039,17 +22049,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$ then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
+      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$, and for all primes $p$ there exists $n$ such that $p^{k-2}\\nmid f(n)$, then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "05 March 2026",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/978",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/978.lean",
       "oeis_urls": [],
       "comments_problem_id": 978,
-      "comments_count": 8
+      "comments_count": 16
     },
     {
       "problem_id": 979,
@@ -22203,7 +22213,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -22368,7 +22378,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 994,
@@ -22435,8 +22445,8 @@
     {
       "problem_id": 997,
       "problem_url": "/997",
-      "status_bucket": "open",
-      "status_dom_id": "open",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
@@ -22446,13 +22456,13 @@
         "discrepancy",
         "primes"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/997",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/997.lean",
       "oeis_urls": [],
       "comments_problem_id": 997,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 998,
@@ -22723,7 +22733,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1010,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1011,
@@ -23131,12 +23141,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "If $R(k,l)$ is the Ramsey number then prove the existence of some $c>0$ such that\\[\\lim_k \\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
+      "statement": "Let $R(k,l)$ be the usual Ramsey number: the smallest $n$ such that if the edges of $K_n$ are coloured red and blue then there exists either a red $K_k$ or a blue $K_l$. Prove the existence of some $c>0$ such that\\[\\lim_{k\\to \\infty}\\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "03 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/1030",
       "formalized": false,
       "formalized_url": "",
@@ -23145,7 +23155,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1031,
@@ -23306,7 +23316,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1038.lean",
       "oeis_urls": [],
       "comments_problem_id": 1038,
-      "comments_count": 127
+      "comments_count": 134
     },
     {
       "problem_id": 1039,
@@ -23327,7 +23337,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -23347,7 +23357,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -23368,7 +23378,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1041.lean",
       "oeis_urls": [],
       "comments_problem_id": 1041,
-      "comments_count": 2
+      "comments_count": 41
     },
     {
       "problem_id": 1042,
@@ -23435,8 +23445,8 @@
       "problem_url": "/1045",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $z_1,\\ldots,z_n\\in \\mathbb{C}$ with $\\lvert z_i-z_j\\rvert\\leq 2$ for all $i,j$, and\\[\\Delta(z_1,\\ldots,z_n)=\\prod_{i\\neq j}\\lvert z_i-z_j\\rvert.\\]What is the maximum possible value of $\\Delta$? Is it maximised by taking the $z_i$ to be the vertices of a regular polygon?",
       "tags": [
@@ -23448,7 +23458,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1046,
@@ -23528,7 +23538,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1049.lean",
       "oeis_urls": [],
       "comments_problem_id": 1049,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 1050,
@@ -24074,7 +24084,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -24516,7 +24526,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -24557,7 +24567,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1097.lean",
       "oeis_urls": [],
       "comments_problem_id": 1097,
-      "comments_count": 11
+      "comments_count": 17
     },
     {
       "problem_id": 1098,
@@ -24683,7 +24693,7 @@
         "https://oeis.org/A392164"
       ],
       "comments_problem_id": 1103,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 1104,
@@ -24841,7 +24851,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -25066,7 +25076,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1121,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 1122,
@@ -25086,7 +25096,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1123,
@@ -25100,7 +25110,7 @@
       "tags": [
         "algebra"
       ],
-      "last_edited": "31 December 2025",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1123",
       "formalized": false,
       "formalized_url": "",
@@ -25294,7 +25304,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -25490,7 +25500,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -25505,7 +25515,7 @@
         "number theory",
         "primes"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1142",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1142.lean",
@@ -25513,7 +25523,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -25622,16 +25632,16 @@
     {
       "problem_id": 1148,
       "problem_url": "/1148",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\\max(x^2,y^2,z^2)\\leq n$?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "26 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/1148",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1148.lean",
@@ -25640,7 +25650,7 @@
         "https://oeis.org/A393168"
       ],
       "comments_problem_id": 1148,
-      "comments_count": 6
+      "comments_count": 26
     },
     {
       "problem_id": 1149,
@@ -25744,7 +25754,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -26163,8 +26173,8 @@
       "problem_url": "/1174",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_3$? Does there exist a graph $G$ with no $K_{\\aleph_1}$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_{\\aleph_0}$?",
       "tags": [
@@ -26177,7 +26187,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -26205,8 +26215,8 @@
       "problem_url": "/1176",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Let $G$ be a graph with chromatic number $\\aleph_1$. Is it true that there is a colouring of the edges with $\\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?",
       "tags": [
@@ -26219,7 +26229,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1176.lean",
       "oeis_urls": [],
       "comments_problem_id": 1176,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1177,
@@ -26284,6 +26294,88 @@
       "oeis_urls": [],
       "comments_problem_id": 1179,
       "comments_count": 0
+    },
+    {
+      "problem_id": 1180,
+      "problem_url": "/1180",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED",
+      "status_detail": "This has been solved in the affirmative.",
+      "prize_amount": "",
+      "statement": "Let $\\epsilon>0$. Does there exist a constant $C_\\epsilon$ such that, for all primes $p$, every residue modulo $p$ is the sum of at most $C_\\epsilon$ many elements of\\[\\{ n^{-1} : 1\\leq n\\leq p^\\epsilon\\}\\]where $n^{-1}$ denotes the inverse of $n$ modulo $p$?",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "06 March 2026",
+      "latex_path": "/latex/1180",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1180,
+      "comments_count": 0
+    },
+    {
+      "problem_id": 1181,
+      "problem_url": "/1181",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $q(n,k)$ denote the least prime which does not divide $\\prod_{1\\leq i\\leq k}(n+i)$. Is it true that there exists some $c>0$ such that, for all large $n$,\\[q(n,\\log n)<(1-c)(\\log n)^2?\\]",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "07 March 2026",
+      "latex_path": "/latex/1181",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1181,
+      "comments_count": 0
+    },
+    {
+      "problem_id": 1182,
+      "problem_url": "/1182",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that there is a connected graph $G$ with $n$ vertices and $f(n)$ edges such that\\[R(K_3,G)= 2n-1.\\]Let $F(n)$ be maximal such that every connected graph $G$ with $n$ vertices and $\\leq F(n)$ edges has\\[R(K_3,G)= 2n-1.\\]Estimate $f(n)$ and $F(n)$. In particular, is it true that $F(n)/n\\to \\infty$?",
+      "tags": [
+        "graph theory",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1182",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1182,
+      "comments_count": 3
+    },
+    {
+      "problem_id": 1183,
+      "problem_url": "/1183",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that in any $2$-colouring of the subsets of $\\{1,\\ldots,n\\}$ there is always a monochromatic family of at least $f(n)$ sets which is closed under taking unions and intersections. Estimate $f(n)$. Let $F(n)$ be defined similarly, except that we only require the family be closed under taking unions. Estimate $F(n)$. In particular, is it true that $F(n)\\geq n^{\\omega(n)}$ for some $\\omega(n)\\to \\infty$ as $n\\to \\infty$, and $F(n)<(1+o(1))^n$?",
+      "tags": [
+        "combinatorics",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1183",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1183,
+      "comments_count": 10
     }
   ]
 }
diff --git a/packs/erdos-open-problems/data/erdos_problems.closed.json b/packs/erdos-open-problems/data/erdos_problems.closed.json
index 310d4b8..98449d4 100644
--- a/packs/erdos-open-problems/data/erdos_problems.closed.json
+++ b/packs/erdos-open-problems/data/erdos_problems.closed.json
@@ -2,32 +2,33 @@
   "schema_version": "1.0.0",
   "subset": "closed",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-04-01T06:51:20Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "870c67de08d4d2a7667ad4a3cd9b930d3a9809cca047a50fa20ab5b2b22fc23d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "495 solved out of 1183 shown",
+      "solved": 495,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 488,
+    "total": 495,
     "open": 0,
-    "closed": 488,
+    "closed": 495,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 7,
-      "DISPROVED": 76,
-      "DISPROVED (LEAN)": 39,
+      "DISPROVED": 75,
+      "DISPROVED (LEAN)": 42,
       "INDEPENDENT": 3,
       "NOT PROVABLE": 1,
-      "PROVED": 237,
-      "PROVED (LEAN)": 63,
-      "SOLVED": 52,
-      "SOLVED (LEAN)": 10
+      "OPEN": 1,
+      "PROVED": 235,
+      "PROVED (LEAN)": 69,
+      "SOLVED": 51,
+      "SOLVED (LEAN)": 11
     }
   },
   "problem_ids": [
@@ -81,6 +82,7 @@
     116,
     118,
     121,
+    125,
     127,
     133,
     134,
@@ -222,6 +224,7 @@
     448,
     449,
     453,
+    457,
     459,
     464,
     465,
@@ -305,6 +308,7 @@
     646,
     648,
     649,
+    650,
     651,
     652,
     656,
@@ -402,6 +406,7 @@
     877,
     880,
     882,
+    884,
     894,
     895,
     897,
@@ -445,6 +450,7 @@
     991,
     992,
     994,
+    997,
     998,
     999,
     1000,
@@ -513,12 +519,14 @@
     1136,
     1140,
     1147,
+    1148,
     1149,
     1161,
     1164,
     1165,
     1166,
-    1179
+    1179,
+    1180
   ],
   "problems": [
     {
@@ -670,7 +678,7 @@
         "graph theory",
         "chromatic number"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/19",
       "formalized": false,
       "formalized_url": "",
@@ -1611,6 +1619,29 @@
       "comments_problem_id": 121,
       "comments_count": 0
     },
+    {
+      "problem_id": 125,
+      "problem_url": "/125",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
+      "prize_amount": "",
+      "statement": "Let $A = \\{ \\sum\\epsilon_k3^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $3$, and $B=\\{ \\sum\\epsilon_k4^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $4$. Does $A+B$ have positive lower density?",
+      "tags": [
+        "number theory",
+        "base representations"
+      ],
+      "last_edited": "30 March 2026",
+      "latex_path": "/latex/125",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/125.lean",
+      "oeis_urls": [
+        "https://oeis.org/A367090"
+      ],
+      "comments_problem_id": 125,
+      "comments_count": 21
+    },
     {
       "problem_id": 127,
       "problem_url": "/127",
@@ -1810,8 +1841,8 @@
       "problem_url": "/150",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let $c(n)$ be the maximum number of minimal cuts a graph on $n$ vertices can have. Does $c(n)^{1/n}\\to \\alpha$ for some $\\alpha <2$?",
       "tags": [
@@ -1823,7 +1854,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 150,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 154,
@@ -2024,12 +2055,12 @@
       "status_dom_id": "solved",
       "status_label": "PROVED",
       "status_detail": "This has been solved in the affirmative.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "Let $k\\geq 3$. What is the maximum number of edges that a graph on $n$ vertices can contain if it does not have a $k$-regular subgraph? Is it $\\ll n^{1+o(1)}$?",
       "tags": [
         "graph theory"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/182",
       "formalized": false,
       "formalized_url": "",
@@ -2211,8 +2242,8 @@
       "problem_url": "/204",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "DISPROVED",
-      "status_detail": "This has been solved in the negative.",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Are there $n$ such that there is a covering system with moduli the divisors of $n$ which is 'as disjoint as possible'? That is, for all $d\\mid n$ with $d>1$ there is an associated $a_d$ such that every integer is congruent to some $a_d\\pmod{d}$, and if there is some integer $x$ with\\[x\\equiv a_d\\pmod{d}\\textrm{ and }x\\equiv a_{d'}\\pmod{d'}\\]then $(d,d')=1$.",
       "tags": [
@@ -2225,7 +2256,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/204.lean",
       "oeis_urls": [],
       "comments_problem_id": 204,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 205,
@@ -2483,7 +2514,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 221,
-      "comments_count": 2
+      "comments_count": 4
     },
     {
       "problem_id": 223,
@@ -2538,7 +2569,7 @@
       "tags": [
         "analysis"
       ],
-      "last_edited": "01 February 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/225",
       "formalized": false,
       "formalized_url": "",
@@ -3270,7 +3301,7 @@
         "number theory",
         "unit fractions"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/298",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/298.lean",
@@ -3448,7 +3479,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 314,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 315,
@@ -3724,7 +3755,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/355.lean",
       "oeis_urls": [],
       "comments_problem_id": 355,
-      "comments_count": 16
+      "comments_count": 18
     },
     {
       "problem_id": 356,
@@ -3791,8 +3822,8 @@
       "problem_url": "/363",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "DISPROVED",
-      "status_detail": "This has been solved in the negative.",
+      "status_label": "DISPROVED (LEAN)",
+      "status_detail": "This has been solved in the negative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Is it true that there are only finitely many collections of disjoint intervals $I_1,\\ldots,I_n$ of size $\\lvert I_i\\rvert \\geq 4$ for $1\\leq i\\leq n$ such that\\[\\prod_{1\\leq i\\leq n}\\prod_{m\\in I_i}m\\]is a square?",
       "tags": [
@@ -3804,7 +3835,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 363,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 370,
@@ -4584,13 +4615,35 @@
       "comments_problem_id": 453,
       "comments_count": 1
     },
+    {
+      "problem_id": 457,
+      "problem_url": "/457",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
+      "prize_amount": "",
+      "statement": "Is there some $\\epsilon>0$ such that there are infinitely many $n$ where all primes $p\\leq (2+\\epsilon)\\log n$ divide\\[\\prod_{1\\leq i\\leq \\log n}(n+i)?\\]",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "07 March 2026",
+      "latex_path": "/latex/457",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/457.lean",
+      "oeis_urls": [
+        "https://oeis.org/A391668"
+      ],
+      "comments_problem_id": 457,
+      "comments_count": 10
+    },
     {
       "problem_id": 459,
       "problem_url": "/459",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "SOLVED",
-      "status_detail": "This has been resolved in some other way than a proof or disproof.",
+      "status_label": "SOLVED (LEAN)",
+      "status_detail": "This has been resolved in some other way than a proof or disproof, and that resolution verified in Lean.",
       "prize_amount": "",
       "statement": "Let $f(u)$ be the largest $v$ such that no $m\\in (u,v)$ is composed entirely of primes dividing $uv$. Estimate $f(u)$.",
       "tags": [
@@ -4605,7 +4658,7 @@
         "https://oeis.org/A289280"
       ],
       "comments_problem_id": 459,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 464,
@@ -4954,7 +5007,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/494.lean",
       "oeis_urls": [],
       "comments_problem_id": 494,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 496,
@@ -5427,7 +5480,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/540",
       "formalized": false,
       "formalized_url": "",
@@ -6313,6 +6366,28 @@
       "comments_problem_id": 649,
       "comments_count": 2
     },
+    {
+      "problem_id": 650,
+      "problem_url": "/650",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
+      "prize_amount": "",
+      "statement": "Let $f(m)$ be such that if $A\\subseteq \\{1,\\ldots,N\\}$ has $\\lvert A\\rvert=m$ then every interval in $[1,\\infty)$ of length $2N$ contains $\\geq f(m)$ many distinct integers $b_1,\\ldots,b_r$ where each $b_i$ is divisible by some $a_i\\in A$, where $a_1,\\ldots,a_r$ are distinct. Estimate $f(m)$. In particular is it true that $f(m)\\leq \\sqrt{m}$?",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "01 April 2026",
+      "latex_path": "/latex/650",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [
+        "https://oeis.org/A027434"
+      ],
+      "comments_problem_id": 650,
+      "comments_count": 28
+    },
     {
       "problem_id": 651,
       "problem_url": "/651",
@@ -6782,7 +6857,7 @@
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "26 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/720",
       "formalized": false,
       "formalized_url": "",
@@ -6832,7 +6907,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 722,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 728,
@@ -6853,7 +6928,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/728.lean",
       "oeis_urls": [],
       "comments_problem_id": 728,
-      "comments_count": 84
+      "comments_count": 86
     },
     {
       "problem_id": 729,
@@ -7191,8 +7266,8 @@
       "problem_url": "/756",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $A\\subset \\mathbb{R}^2$ be a set of $n$ points. Can there be $\\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$?",
       "tags": [
@@ -7205,7 +7280,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 756,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 758,
@@ -7528,20 +7603,20 @@
       "problem_url": "/785",
       "status_bucket": "closed",
       "status_dom_id": "solved",
-      "status_label": "PROVED",
-      "status_detail": "This has been solved in the affirmative.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $A,B\\subseteq \\mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\\lvert A\\cap [1,x]\\rvert$ and similarly for $B(x)$. Is it true that if $A(x)B(x)\\sim x$ then\\[A(x)B(x)-x\\to \\infty\\]as $x\\to \\infty$?",
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/785",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 785,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 794,
@@ -8145,7 +8220,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/848.lean",
       "oeis_urls": [],
       "comments_problem_id": 848,
-      "comments_count": 18
+      "comments_count": 47
     },
     {
       "problem_id": 861,
@@ -8341,6 +8416,27 @@
       "comments_problem_id": 882,
       "comments_count": 0
     },
+    {
+      "problem_id": 884,
+      "problem_url": "/884",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "DISPROVED",
+      "status_detail": "This has been solved in the negative.",
+      "prize_amount": "",
+      "statement": "Is it true that, for any $n$, if $d_1<\\cdots <d_t$ are the divisors of $n$, then\\[\\sum_{1\\leq i<j\\leq t}\\frac{1}{d_j-d_i} \\ll 1+\\sum_{1\\leq i<t}\\frac{1}{d_{i+1}-d_i},\\]where the implied constant is absolute?",
+      "tags": [
+        "number theory",
+        "divisors"
+      ],
+      "last_edited": "01 April 2026",
+      "latex_path": "/latex/884",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 884,
+      "comments_count": 10
+    },
     {
       "problem_id": 894,
       "problem_url": "/894",
@@ -8455,7 +8551,7 @@
       "tags": [
         "graph theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/900",
       "formalized": false,
       "formalized_url": "",
@@ -8622,7 +8718,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 914,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 915,
@@ -8727,7 +8823,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 923,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 924,
@@ -9234,6 +9330,28 @@
       "comments_problem_id": 994,
       "comments_count": 0
     },
+    {
+      "problem_id": 997,
+      "problem_url": "/997",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Call $x_1,x_2,\\ldots \\in (0,1)$ well-distributed if, for every $\\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\\subseteq [0,1]$,\\[\\lvert \\# \\{ n<m\\leq n+k : x_m\\in I\\} - \\lvert I\\rvert k\\rvert < \\epsilon k.\\]Is it true that, for every $\\alpha$, the sequence $\\{ \\alpha p_n\\}$ is not well-distributed, if $p_n$ is the sequence of primes?",
+      "tags": [
+        "analysis",
+        "discrepancy",
+        "primes"
+      ],
+      "last_edited": "01 April 2026",
+      "latex_path": "/latex/997",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/997.lean",
+      "oeis_urls": [],
+      "comments_problem_id": 997,
+      "comments_count": 2
+    },
     {
       "problem_id": 998,
       "problem_url": "/998",
@@ -9418,7 +9536,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1010,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1012,
@@ -10384,7 +10502,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1121,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 1123,
@@ -10398,7 +10516,7 @@
       "tags": [
         "algebra"
       ],
-      "last_edited": "31 December 2025",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1123",
       "formalized": false,
       "formalized_url": "",
@@ -10635,6 +10753,29 @@
       "comments_problem_id": 1147,
       "comments_count": 2
     },
+    {
+      "problem_id": 1148,
+      "problem_url": "/1148",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
+      "prize_amount": "",
+      "statement": "Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\\max(x^2,y^2,z^2)\\leq n$?",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "23 March 2026",
+      "latex_path": "/latex/1148",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1148.lean",
+      "oeis_urls": [
+        "https://oeis.org/A390380",
+        "https://oeis.org/A393168"
+      ],
+      "comments_problem_id": 1148,
+      "comments_count": 26
+    },
     {
       "problem_id": 1149,
       "problem_url": "/1149",
@@ -10755,6 +10896,26 @@
       "oeis_urls": [],
       "comments_problem_id": 1179,
       "comments_count": 0
+    },
+    {
+      "problem_id": 1180,
+      "problem_url": "/1180",
+      "status_bucket": "closed",
+      "status_dom_id": "solved",
+      "status_label": "PROVED",
+      "status_detail": "This has been solved in the affirmative.",
+      "prize_amount": "",
+      "statement": "Let $\\epsilon>0$. Does there exist a constant $C_\\epsilon$ such that, for all primes $p$, every residue modulo $p$ is the sum of at most $C_\\epsilon$ many elements of\\[\\{ n^{-1} : 1\\leq n\\leq p^\\epsilon\\}\\]where $n^{-1}$ denotes the inverse of $n$ modulo $p$?",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "06 March 2026",
+      "latex_path": "/latex/1180",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1180,
+      "comments_count": 0
     }
   ]
 }
diff --git a/packs/erdos-open-problems/data/erdos_problems.open.json b/packs/erdos-open-problems/data/erdos_problems.open.json
index ba08458..b9cc68d 100644
--- a/packs/erdos-open-problems/data/erdos_problems.open.json
+++ b/packs/erdos-open-problems/data/erdos_problems.open.json
@@ -2,30 +2,32 @@
   "schema_version": "1.0.0",
   "subset": "open",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-04-01T06:51:20Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "870c67de08d4d2a7667ad4a3cd9b930d3a9809cca047a50fa20ab5b2b22fc23d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "495 solved out of 1183 shown",
+      "solved": 495,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 691,
-    "open": 691,
+    "total": 688,
+    "open": 688,
     "closed": 0,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 2,
+      "DISPROVED": 1,
       "DISPROVED (LEAN)": 1,
-      "FALSIFIABLE": 29,
-      "NOT DISPROVABLE": 2,
+      "FALSIFIABLE": 27,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 3,
-      "OPEN": 645,
-      "PROVED": 2,
+      "OPEN": 639,
+      "PROVED": 3,
+      "PROVED (LEAN)": 1,
       "VERIFIABLE": 7
     }
   },
@@ -104,7 +106,6 @@
     122,
     123,
     124,
-    125,
     126,
     128,
     129,
@@ -295,7 +296,6 @@
     454,
     455,
     456,
-    457,
     458,
     460,
     461,
@@ -405,7 +405,6 @@
     643,
     644,
     647,
-    650,
     653,
     654,
     655,
@@ -542,7 +541,6 @@
     879,
     881,
     883,
-    884,
     885,
     886,
     887,
@@ -612,7 +610,6 @@
     993,
     995,
     996,
-    997,
     1002,
     1003,
     1004,
@@ -695,7 +692,6 @@
     1144,
     1145,
     1146,
-    1148,
     1150,
     1151,
     1152,
@@ -720,7 +716,10 @@
     1175,
     1176,
     1177,
-    1178
+    1178,
+    1181,
+    1182,
+    1183
   ],
   "problems": [
     {
@@ -870,8 +869,8 @@
       "problem_url": "/11",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Is every large odd integer $n$ the sum of a squarefree number and a power of 2?",
       "tags": [
@@ -993,8 +992,8 @@
       ],
       "last_edited": "20 January 2026",
       "latex_path": "/latex/18",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/18.lean",
       "oeis_urls": [
         "https://oeis.org/A005153"
       ],
@@ -1013,7 +1012,7 @@
       "tags": [
         "combinatorics"
       ],
-      "last_edited": "25 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/20",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/20.lean",
@@ -1063,7 +1062,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/25.lean",
       "oeis_urls": [],
       "comments_problem_id": 25,
-      "comments_count": 2
+      "comments_count": 7
     },
     {
       "problem_id": 28,
@@ -1152,7 +1151,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/33.lean",
       "oeis_urls": [],
       "comments_problem_id": 33,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 36,
@@ -1346,8 +1345,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/50",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/50.lean",
       "oeis_urls": [],
       "comments_problem_id": 50,
       "comments_count": 0
@@ -1388,7 +1387,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/52",
       "formalized": false,
       "formalized_url": "",
@@ -1747,8 +1746,8 @@
       "problem_url": "/85",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $n\\geq 4$ and $f(n)$ be minimal such that every graph on $n$ vertices with minimal degree $\\geq f(n)$ contains a $C_4$. Is it true that, for all large $n$, $f(n+1)\\geq f(n)$?",
       "tags": [
@@ -1878,7 +1877,7 @@
         "https://oeis.org/A186704"
       ],
       "comments_problem_id": 91,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 92,
@@ -2105,7 +2104,7 @@
       "tags": [
         "geometry"
       ],
-      "last_edited": "",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/106",
       "formalized": false,
       "formalized_url": "",
@@ -2206,8 +2205,8 @@
       "problem_url": "/114",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "$250",
       "statement": "If $p(z)\\in\\mathbb{C}[z]$ is a monic polynomial of degree $n$ then is the length of the curve $\\{ z\\in \\mathbb{C} : \\lvert p(z)\\rvert=1\\}$ maximised when $p(z)=z^n-1$?",
       "tags": [
@@ -2220,7 +2219,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 114,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 117,
@@ -2281,7 +2280,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/120.lean",
       "oeis_urls": [],
       "comments_problem_id": 120,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 122,
@@ -2301,7 +2300,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 122,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 123,
@@ -2345,29 +2344,6 @@
       "comments_problem_id": 124,
       "comments_count": 13
     },
-    {
-      "problem_id": 125,
-      "problem_url": "/125",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Let $A = \\{ \\sum\\epsilon_k3^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $3$, and $B=\\{ \\sum\\epsilon_k4^k : \\epsilon_k\\in \\{0,1\\}\\}$ be the set of integers which have only the digits $0,1$ when written base $4$. Does $A+B$ have positive density?",
-      "tags": [
-        "number theory",
-        "base representations"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/125",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/125.lean",
-      "oeis_urls": [
-        "https://oeis.org/A367090"
-      ],
-      "comments_problem_id": 125,
-      "comments_count": 13
-    },
     {
       "problem_id": 126,
       "problem_url": "/126",
@@ -2826,13 +2802,13 @@
       "status_dom_id": "open",
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "There exists some constant $c>0$ such that $$R(C_4,K_n) \\ll n^{2-c}.$$",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/159",
       "formalized": false,
       "formalized_url": "",
@@ -2919,7 +2895,7 @@
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/165",
       "formalized": false,
       "formalized_url": "",
@@ -2961,7 +2937,7 @@
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "24 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/168",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/168.lean",
@@ -3102,7 +3078,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 176,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 177,
@@ -3205,11 +3181,11 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/184",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/184.lean",
       "oeis_urls": [],
       "comments_problem_id": 184,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 187,
@@ -3289,8 +3265,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/193",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/193.lean",
       "oeis_urls": [
         "https://oeis.org/A231255"
       ],
@@ -3693,7 +3669,7 @@
         "https://oeis.org/A387704"
       ],
       "comments_problem_id": 241,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 242,
@@ -3744,7 +3720,7 @@
         "https://oeis.org/A000058"
       ],
       "comments_problem_id": 243,
-      "comments_count": 6
+      "comments_count": 7
     },
     {
       "problem_id": 244,
@@ -3872,8 +3848,8 @@
       ],
       "last_edited": "07 December 2025",
       "latex_path": "/latex/254",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/254.lean",
       "oeis_urls": [],
       "comments_problem_id": 254,
       "comments_count": 3
@@ -3952,8 +3928,8 @@
       ],
       "last_edited": "01 February 2026",
       "latex_path": "/latex/260",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/260.lean",
       "oeis_urls": [],
       "comments_problem_id": 260,
       "comments_count": 2
@@ -4162,7 +4138,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/274.lean",
       "oeis_urls": [],
       "comments_problem_id": 274,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 276,
@@ -4270,7 +4246,7 @@
         "https://oeis.org/A380791"
       ],
       "comments_problem_id": 283,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 287,
@@ -4723,8 +4699,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/323",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/323.lean",
       "oeis_urls": [],
       "comments_problem_id": 323,
       "comments_count": 0
@@ -4769,7 +4745,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/325.lean",
       "oeis_urls": [],
       "comments_problem_id": 325,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 326,
@@ -4790,7 +4766,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/326.lean",
       "oeis_urls": [],
       "comments_problem_id": 326,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 327,
@@ -4849,7 +4825,7 @@
         "number theory",
         "additive basis"
       ],
-      "last_edited": "08 December 2025",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/330",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/330.lean",
@@ -4893,7 +4869,10 @@
       "latex_path": "/latex/334",
       "formalized": false,
       "formalized_url": "",
-      "oeis_urls": [],
+      "oeis_urls": [
+        "https://oeis.org/A045535",
+        "https://oeis.org/A062241"
+      ],
       "comments_problem_id": 334,
       "comments_count": 2
     },
@@ -5019,13 +4998,13 @@
       ],
       "last_edited": "30 September 2025",
       "latex_path": "/latex/342",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/342.lean",
       "oeis_urls": [
         "https://oeis.org/A002858"
       ],
       "comments_problem_id": 342,
-      "comments_count": 11
+      "comments_count": 18
     },
     {
       "problem_id": 345,
@@ -5111,7 +5090,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/349.lean",
       "oeis_urls": [],
       "comments_problem_id": 349,
-      "comments_count": 8
+      "comments_count": 12
     },
     {
       "problem_id": 351,
@@ -5218,7 +5197,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/358.lean",
       "oeis_urls": [],
       "comments_problem_id": 358,
-      "comments_count": 19
+      "comments_count": 21
     },
     {
       "problem_id": 359,
@@ -5309,7 +5288,7 @@
         "https://oeis.org/A175155"
       ],
       "comments_problem_id": 365,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 366,
@@ -5319,12 +5298,12 @@
       "status_label": "VERIFIABLE",
       "status_detail": "Open, but could be proved with a finite example.",
       "prize_amount": "",
-      "statement": "Are there any 2-full $n$ such that $n+1$ is 3-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
+      "statement": "Are there any $2$-full $n$ such that $n+1$ is $3$-full? That is, if $p\\mid n$ then $p^2\\mid n$ and if $p\\mid n+1$ then $p^3\\mid n+1$.",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "20 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/366",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/366.lean",
@@ -5342,12 +5321,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $B_2(n)$ be the 2-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
+      "statement": "Let $B_2(n)$ be the $2$-full part of $n$ (that is, $B_2(n)=n/n'$ where $n'$ is the product of all primes that divide $n$ exactly once). Is it true that, for every fixed $k\\geq 1$,\\[\\prod_{n\\leq m<n+k}B_2(m) \\ll n^{2+o(1)}?\\]Or perhaps even $\\ll_k n^2$?",
       "tags": [
         "number theory",
         "powerful"
       ],
-      "last_edited": "08 February 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/367",
       "formalized": false,
       "formalized_url": "",
@@ -5384,8 +5363,8 @@
       "problem_url": "/369",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED (LEAN)",
+      "status_detail": "This has been solved in the affirmative and the proof verified in Lean.",
       "prize_amount": "",
       "statement": "Let $\\epsilon>0$ and $k\\geq 2$. Is it true that, for all sufficiently large $n$, there is a sequence of $k$ consecutive integers in $\\{1,\\ldots,n\\}$ all of which are $n^\\epsilon$-smooth?",
       "tags": [
@@ -5397,7 +5376,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 369,
-      "comments_count": 0
+      "comments_count": 11
     },
     {
       "problem_id": 371,
@@ -5467,7 +5446,7 @@
         "https://oeis.org/A389148"
       ],
       "comments_problem_id": 374,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 375,
@@ -5540,8 +5519,8 @@
       "problem_url": "/380",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "PROVED",
+      "status_detail": "This has been solved in the affirmative.",
       "prize_amount": "",
       "statement": "We call an interval $[u,v]$ 'bad' if the greatest prime factor of $\\prod_{u\\leq m\\leq v}m$ occurs with an exponent greater than $1$. Let $B(x)$ count the number of $n\\leq x$ which are contained in at least one bad interval. Is it true that\\[B(x)\\sim \\#\\{ n\\leq x: P(n)^2\\mid n\\},\\]where $P(n)$ is the largest prime factor of $n$?",
       "tags": [
@@ -5558,7 +5537,7 @@
         "https://oeis.org/A389100"
       ],
       "comments_problem_id": 380,
-      "comments_count": 5
+      "comments_count": 9
     },
     {
       "problem_id": 382,
@@ -5645,7 +5624,7 @@
         "https://oeis.org/A280992"
       ],
       "comments_problem_id": 386,
-      "comments_count": 12
+      "comments_count": 13
     },
     {
       "problem_id": 387,
@@ -5686,7 +5665,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -5708,7 +5687,7 @@
         "https://oeis.org/A375071"
       ],
       "comments_problem_id": 389,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 390,
@@ -5799,7 +5778,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 30
     },
     {
       "problem_id": 398,
@@ -5814,15 +5793,16 @@
         "number theory",
         "factorials"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/398",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/398.lean",
       "oeis_urls": [
+        "https://oeis.org/A141399",
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 9
     },
     {
       "problem_id": 400,
@@ -5839,8 +5819,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/400",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/400.lean",
       "oeis_urls": [],
       "comments_problem_id": 400,
       "comments_count": 0
@@ -6192,7 +6172,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -6200,7 +6180,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -6214,7 +6194,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/424",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/424.lean",
@@ -6363,8 +6343,8 @@
       ],
       "last_edited": "27 December 2025",
       "latex_path": "/latex/445",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/445.lean",
       "oeis_urls": [],
       "comments_problem_id": 445,
       "comments_count": 1
@@ -6496,28 +6476,6 @@
       "comments_problem_id": 456,
       "comments_count": 2
     },
-    {
-      "problem_id": 457,
-      "problem_url": "/457",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Is there some $\\epsilon>0$ such that there are infinitely many $n$ where all primes $p\\leq (2+\\epsilon)\\log n$ divide\\[\\prod_{1\\leq i\\leq \\log n}(n+i)?\\]",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "07 October 2025",
-      "latex_path": "/latex/457",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/457.lean",
-      "oeis_urls": [
-        "https://oeis.org/A391668"
-      ],
-      "comments_problem_id": 457,
-      "comments_count": 7
-    },
     {
       "problem_id": 458,
       "problem_url": "/458",
@@ -6775,7 +6733,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -6904,8 +6862,8 @@
       "problem_url": "/488",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "FALSIFIABLE",
+      "status_detail": "Open, but could be disproved with a finite counterexample.",
       "prize_amount": "",
       "statement": "Let $A$ be a finite set and\\[B=\\{ n \\geq 1 : a\\mid n\\textrm{ for some }a\\in A\\}.\\]Is it true that, for every $m>n\\geq \\max(A)$,\\[\\frac{\\lvert B\\cap [1,m]\\rvert }{m}< 2\\frac{\\lvert B\\cap [1,n]\\rvert}{n}?\\]",
       "tags": [
@@ -6917,7 +6875,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/488.lean",
       "oeis_urls": [],
       "comments_problem_id": 488,
-      "comments_count": 14
+      "comments_count": 27
     },
     {
       "problem_id": 489,
@@ -7168,7 +7126,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/517.lean",
       "oeis_urls": [],
       "comments_problem_id": 517,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 520,
@@ -7478,12 +7436,12 @@
       "status_dom_id": "open",
       "status_label": "FALSIFIABLE",
       "status_detail": "Open, but could be disproved with a finite counterexample.",
-      "prize_amount": "",
+      "prize_amount": "$100",
       "statement": "Let $n\\geq k+1$. Every graph on $n$ vertices with at least $\\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.",
       "tags": [
         "graph theory"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/548",
       "formalized": false,
       "formalized_url": "",
@@ -7809,7 +7767,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 569,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 571,
@@ -7824,7 +7782,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -7882,8 +7840,8 @@
       "problem_url": "/574",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "DISPROVED",
+      "status_detail": "This has been solved in the negative.",
       "prize_amount": "",
       "statement": "Is it true that, for $k\\geq 2$,\\[\\mathrm{ex}(n;\\{C_{2k-1},C_{2k}\\})=(1+o(1))(n/2)^{1+\\frac{1}{k}}.\\]",
       "tags": [
@@ -7896,7 +7854,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 574,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 575,
@@ -7999,7 +7957,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -8211,7 +8169,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/598.lean",
       "oeis_urls": [],
       "comments_problem_id": 598,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 600,
@@ -8309,7 +8267,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -8456,7 +8414,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/617.lean",
       "oeis_urls": [],
       "comments_problem_id": 617,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 619,
@@ -8662,7 +8620,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -8831,26 +8789,6 @@
       "comments_problem_id": 647,
       "comments_count": 6
     },
-    {
-      "problem_id": 650,
-      "problem_url": "/650",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Let $f(m)$ be such that if $A\\subseteq \\{1,\\ldots,N\\}$ has $\\lvert A\\rvert=m$ then every interval in $[1,\\infty)$ of length $2N$ contains $\\geq f(m)$ many distinct integers $b_1,\\ldots,b_r$ where each $b_i$ is divisible by some $a_i\\in A$, where $a_1,\\ldots,a_r$ are distinct. Estimate $f(m)$. In particular is it true that $f(m)\\ll m^{1/2}$?",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/650",
-      "formalized": false,
-      "formalized_url": "",
-      "oeis_urls": [],
-      "comments_problem_id": 650,
-      "comments_count": 0
-    },
     {
       "problem_id": 653,
       "problem_url": "/653",
@@ -9228,7 +9166,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/677.lean",
       "oeis_urls": [],
       "comments_problem_id": 677,
-      "comments_count": 0
+      "comments_count": 7
     },
     {
       "problem_id": 679,
@@ -9310,8 +9248,8 @@
       ],
       "last_edited": "31 December 2025",
       "latex_path": "/latex/683",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/683.lean",
       "oeis_urls": [
         "https://oeis.org/A006530",
         "https://oeis.org/A074399",
@@ -9334,7 +9272,7 @@
         "primes",
         "binomial coefficients"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/684",
       "formalized": false,
       "formalized_url": "",
@@ -9384,7 +9322,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/686.lean",
       "oeis_urls": [],
       "comments_problem_id": 686,
-      "comments_count": 16
+      "comments_count": 37
     },
     {
       "problem_id": 687,
@@ -9660,7 +9598,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 706,
@@ -9715,13 +9653,13 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/709",
       "formalized": false,
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 709,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 710,
@@ -9800,7 +9738,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "06 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/713",
       "formalized": false,
       "formalized_url": "",
@@ -10118,17 +10056,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
+      "statement": "Let $A\\subseteq \\mathbb{N}$ be such that $A+A$ has positive (upper) density. Can one always decompose $A=A_1\\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive (upper) density? Is there a basis $A$ of order $2$ such that if $A=A_1\\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?",
       "tags": [
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "01 April 2026",
       "latex_path": "/latex/741",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/741.lean",
       "oeis_urls": [],
       "comments_problem_id": 741,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 743,
@@ -10711,7 +10649,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -10770,8 +10708,8 @@
       ],
       "last_edited": "",
       "latex_path": "/latex/812",
-      "formalized": false,
-      "formalized_url": "",
+      "formalized": true,
+      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/812.lean",
       "oeis_urls": [],
       "comments_problem_id": 812,
       "comments_count": 0
@@ -11041,7 +10979,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/835.lean",
       "oeis_urls": [],
       "comments_problem_id": 835,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 836,
@@ -11287,7 +11225,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -11317,8 +11255,8 @@
       "problem_url": "/855",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "If $\\pi(x)$ counts the number of primes in $[1,x]$ then is it true that (for large $x$ and $y$)\\[\\pi(x+y) \\leq \\pi(x)+\\pi(y)?\\]",
       "tags": [
@@ -11738,27 +11676,6 @@
       "comments_problem_id": 883,
       "comments_count": 3
     },
-    {
-      "problem_id": 884,
-      "problem_url": "/884",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Is it true that, for any $n$, if $d_1<\\cdots <d_t$ are the divisors of $n$, then\\[\\sum_{1\\leq i<j\\leq t}\\frac{1}{d_j-d_i} \\ll 1+\\sum_{1\\leq i<t}\\frac{1}{d_{i+1}-d_i},\\]where the implied constant is absolute?",
-      "tags": [
-        "number theory",
-        "divisors"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/884",
-      "formalized": false,
-      "formalized_url": "",
-      "oeis_urls": [],
-      "comments_problem_id": 884,
-      "comments_count": 5
-    },
     {
       "problem_id": 885,
       "problem_url": "/885",
@@ -12264,7 +12181,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/931.lean",
       "oeis_urls": [],
       "comments_problem_id": 931,
-      "comments_count": 0
+      "comments_count": 4
     },
     {
       "problem_id": 932,
@@ -12326,7 +12243,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -12480,7 +12397,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/943.lean",
       "oeis_urls": [],
       "comments_problem_id": 943,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 944,
@@ -12830,7 +12747,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/968",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/968.lean",
@@ -12944,7 +12861,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 975,
@@ -12998,17 +12915,17 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$ then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
+      "statement": "Let $f\\in \\mathbb{Z}[x]$ be an irreducible polynomial of degree $k>2$ (and suppose that $k\\neq 2^l$ for any $l\\geq 1$) such that the leading coefficient of $f$ is positive. Does the set of integers $n\\geq 1$ for which $f(n)$ is $(k-1)$-power-free have positive density? If $k>3$, and for all primes $p$ there exists $n$ such that $p^{k-2}\\nmid f(n)$, then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free? In particular, does\\[n^4+2\\]represent infinitely many squarefree numbers?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "05 March 2026",
+      "last_edited": "31 March 2026",
       "latex_path": "/latex/978",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/978.lean",
       "oeis_urls": [],
       "comments_problem_id": 978,
-      "comments_count": 8
+      "comments_count": 16
     },
     {
       "problem_id": 979,
@@ -13098,7 +13015,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -13183,7 +13100,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 995,
@@ -13226,28 +13143,6 @@
       "comments_problem_id": 996,
       "comments_count": 0
     },
-    {
-      "problem_id": 997,
-      "problem_url": "/997",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Call $x_1,x_2,\\ldots \\in (0,1)$ well-distributed if, for every $\\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\\subseteq [0,1]$,\\[\\lvert \\# \\{ n<m\\leq n+k : x_m\\in I\\} - \\lvert I\\rvert k\\rvert < \\epsilon k.\\]Is it true that, for every $\\alpha$, the sequence $\\{ \\alpha p_n\\}$ is not well-distributed, if $p_n$ is the sequence of primes?",
-      "tags": [
-        "analysis",
-        "discrepancy",
-        "primes"
-      ],
-      "last_edited": "",
-      "latex_path": "/latex/997",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/997.lean",
-      "oeis_urls": [],
-      "comments_problem_id": 997,
-      "comments_count": 0
-    },
     {
       "problem_id": 1002,
       "problem_url": "/1002",
@@ -13490,12 +13385,12 @@
       "status_label": "OPEN",
       "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
-      "statement": "If $R(k,l)$ is the Ramsey number then prove the existence of some $c>0$ such that\\[\\lim_k \\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
+      "statement": "Let $R(k,l)$ be the usual Ramsey number: the smallest $n$ such that if the edges of $K_n$ are coloured red and blue then there exists either a red $K_k$ or a blue $K_l$. Prove the existence of some $c>0$ such that\\[\\lim_{k\\to \\infty}\\frac{R(k+1,k)}{R(k,k)}> 1+c.\\]",
       "tags": [
         "graph theory",
         "ramsey theory"
       ],
-      "last_edited": "03 December 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/1030",
       "formalized": false,
       "formalized_url": "",
@@ -13504,7 +13399,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1032,
@@ -13585,7 +13480,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1038.lean",
       "oeis_urls": [],
       "comments_problem_id": 1038,
-      "comments_count": 127
+      "comments_count": 134
     },
     {
       "problem_id": 1039,
@@ -13606,7 +13501,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -13626,7 +13521,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -13647,15 +13542,15 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1041.lean",
       "oeis_urls": [],
       "comments_problem_id": 1041,
-      "comments_count": 2
+      "comments_count": 41
     },
     {
       "problem_id": 1045,
       "problem_url": "/1045",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "FALSIFIABLE",
-      "status_detail": "Open, but could be disproved with a finite counterexample.",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
       "prize_amount": "",
       "statement": "Let $z_1,\\ldots,z_n\\in \\mathbb{C}$ with $\\lvert z_i-z_j\\rvert\\leq 2$ for all $i,j$, and\\[\\Delta(z_1,\\ldots,z_n)=\\prod_{i\\neq j}\\lvert z_i-z_j\\rvert.\\]What is the maximum possible value of $\\Delta$? Is it maximised by taking the $z_i$ to be the vertices of a regular polygon?",
       "tags": [
@@ -13667,7 +13562,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1049,
@@ -13687,7 +13582,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1049.lean",
       "oeis_urls": [],
       "comments_problem_id": 1049,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 1052,
@@ -14087,7 +13982,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -14362,7 +14257,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -14403,7 +14298,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1097.lean",
       "oeis_urls": [],
       "comments_problem_id": 1097,
-      "comments_count": 11
+      "comments_count": 17
     },
     {
       "problem_id": 1100,
@@ -14468,7 +14363,7 @@
         "https://oeis.org/A392164"
       ],
       "comments_problem_id": 1103,
-      "comments_count": 4
+      "comments_count": 5
     },
     {
       "problem_id": 1104,
@@ -14605,7 +14500,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -14728,7 +14623,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1131,
@@ -14770,7 +14665,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -14904,7 +14799,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -14919,7 +14814,7 @@
         "number theory",
         "primes"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1142",
       "formalized": true,
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1142.lean",
@@ -14927,7 +14822,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -15012,29 +14907,6 @@
       "comments_problem_id": 1146,
       "comments_count": 0
     },
-    {
-      "problem_id": 1148,
-      "problem_url": "/1148",
-      "status_bucket": "open",
-      "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
-      "prize_amount": "",
-      "statement": "Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\\max(x^2,y^2,z^2)\\leq n$?",
-      "tags": [
-        "number theory"
-      ],
-      "last_edited": "26 January 2026",
-      "latex_path": "/latex/1148",
-      "formalized": true,
-      "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1148.lean",
-      "oeis_urls": [
-        "https://oeis.org/A390380",
-        "https://oeis.org/A393168"
-      ],
-      "comments_problem_id": 1148,
-      "comments_count": 6
-    },
     {
       "problem_id": 1150,
       "problem_url": "/1150",
@@ -15117,7 +14989,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -15456,8 +15328,8 @@
       "problem_url": "/1174",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_3$? Does there exist a graph $G$ with no $K_{\\aleph_1}$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_{\\aleph_0}$?",
       "tags": [
@@ -15470,7 +15342,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -15498,8 +15370,8 @@
       "problem_url": "/1176",
       "status_bucket": "open",
       "status_dom_id": "open",
-      "status_label": "OPEN",
-      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "status_label": "NOT DISPROVABLE",
+      "status_detail": "Open in general, but there exist models of set theory where the result is true.",
       "prize_amount": "",
       "statement": "Let $G$ be a graph with chromatic number $\\aleph_1$. Is it true that there is a colouring of the edges with $\\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?",
       "tags": [
@@ -15512,7 +15384,7 @@
       "formalized_url": "https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1176.lean",
       "oeis_urls": [],
       "comments_problem_id": 1176,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1177,
@@ -15556,6 +15428,68 @@
       "oeis_urls": [],
       "comments_problem_id": 1178,
       "comments_count": 1
+    },
+    {
+      "problem_id": 1181,
+      "problem_url": "/1181",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $q(n,k)$ denote the least prime which does not divide $\\prod_{1\\leq i\\leq k}(n+i)$. Is it true that there exists some $c>0$ such that, for all large $n$,\\[q(n,\\log n)<(1-c)(\\log n)^2?\\]",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "07 March 2026",
+      "latex_path": "/latex/1181",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1181,
+      "comments_count": 0
+    },
+    {
+      "problem_id": 1182,
+      "problem_url": "/1182",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that there is a connected graph $G$ with $n$ vertices and $f(n)$ edges such that\\[R(K_3,G)= 2n-1.\\]Let $F(n)$ be maximal such that every connected graph $G$ with $n$ vertices and $\\leq F(n)$ edges has\\[R(K_3,G)= 2n-1.\\]Estimate $f(n)$ and $F(n)$. In particular, is it true that $F(n)/n\\to \\infty$?",
+      "tags": [
+        "graph theory",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1182",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1182,
+      "comments_count": 3
+    },
+    {
+      "problem_id": 1183,
+      "problem_url": "/1183",
+      "status_bucket": "open",
+      "status_dom_id": "open",
+      "status_label": "OPEN",
+      "status_detail": "This is open, and cannot be resolved with a finite computation.",
+      "prize_amount": "",
+      "statement": "Let $f(n)$ be maximal such that in any $2$-colouring of the subsets of $\\{1,\\ldots,n\\}$ there is always a monochromatic family of at least $f(n)$ sets which is closed under taking unions and intersections. Estimate $f(n)$. Let $F(n)$ be defined similarly, except that we only require the family be closed under taking unions. Estimate $F(n)$. In particular, is it true that $F(n)\\geq n^{\\omega(n)}$ for some $\\omega(n)\\to \\infty$ as $n\\to \\infty$, and $F(n)<(1+o(1))^n$?",
+      "tags": [
+        "combinatorics",
+        "ramsey theory"
+      ],
+      "last_edited": "",
+      "latex_path": "/latex/1183",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [],
+      "comments_problem_id": 1183,
+      "comments_count": 10
     }
   ]
 }