diff --git a/packs/erdos-open-problems/data/erdos_open_problems.md b/packs/erdos-open-problems/data/erdos_open_problems.md
index 46e175f..02cdd31 100644
--- a/packs/erdos-open-problems/data/erdos_open_problems.md
+++ b/packs/erdos-open-problems/data/erdos_open_problems.md
@@ -1,6 +1,6 @@
 # Erdos Open Problems (Active Snapshot)
 
-- generated_at_utc: `2026-03-05T15:52:31Z`
+- generated_at_utc: `2026-03-26T06:41:23Z`
 - source_url: `https://erdosproblems.com/range/1-end`
 - total_open: `691`
 
@@ -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,7 +66,7 @@
 - [#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...
@@ -100,13 +100,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...
@@ -254,7 +254,7 @@
 - [#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...
+- [#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 — 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...
@@ -269,7 +269,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,7 +280,7 @@
 - [#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}$?
@@ -314,7 +313,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,7 +329,7 @@
 - [#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}}.\]
@@ -353,7 +352,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 +378,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...
@@ -420,11 +418,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...
@@ -496,7 +494,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$....
@@ -598,7 +596,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 +604,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 +662,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 +687,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..b7b07be 100644
--- a/packs/erdos-open-problems/data/erdos_problems.active.json
+++ b/packs/erdos-open-problems/data/erdos_problems.active.json
@@ -2,15 +2,15 @@
   "schema_version": "1.0.0",
   "subset": "active",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-03-26T06:41:23Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "171716cab9853224a2367a87091d6cb6a953c3ea1c9801050ed043514d81641d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "492 solved out of 1183 shown",
+      "solved": 492,
+      "shown": 1183
     }
   },
   "summary": {
@@ -21,10 +21,10 @@
     "status_label_counts": {
       "DECIDABLE": 2,
       "DISPROVED (LEAN)": 1,
-      "FALSIFIABLE": 29,
-      "NOT DISPROVABLE": 2,
+      "FALSIFIABLE": 25,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 3,
-      "OPEN": 645,
+      "OPEN": 647,
       "PROVED": 2,
       "VERIFIABLE": 7
     }
@@ -295,7 +295,6 @@
     454,
     455,
     456,
-    457,
     458,
     460,
     461,
@@ -405,7 +404,6 @@
     643,
     644,
     647,
-    650,
     653,
     654,
     655,
@@ -695,7 +693,6 @@
     1144,
     1145,
     1146,
-    1148,
     1150,
     1151,
     1152,
@@ -720,7 +717,10 @@
     1175,
     1176,
     1177,
-    1178
+    1178,
+    1181,
+    1182,
+    1183
   ],
   "problems": [
     {
@@ -870,8 +870,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 +993,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 +1013,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 +1063,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 +1152,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 +1346,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 +1388,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 +1747,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 +1878,7 @@
         "https://oeis.org/A186704"
       ],
       "comments_problem_id": 91,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 92,
@@ -2105,7 +2105,7 @@
       "tags": [
         "geometry"
       ],
-      "last_edited": "",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/106",
       "formalized": false,
       "formalized_url": "",
@@ -2281,7 +2281,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,
@@ -2826,13 +2826,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 +2919,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 +2961,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 +3102,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 176,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 177,
@@ -3205,11 +3205,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 +3289,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 +3693,7 @@
         "https://oeis.org/A387704"
       ],
       "comments_problem_id": 241,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 242,
@@ -3744,7 +3744,7 @@
         "https://oeis.org/A000058"
       ],
       "comments_problem_id": 243,
-      "comments_count": 6
+      "comments_count": 7
     },
     {
       "problem_id": 244,
@@ -3872,8 +3872,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 +3952,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 +4162,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,
@@ -4723,8 +4723,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 +4769,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 +4790,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,
@@ -4893,7 +4893,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 +5022,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 +5114,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,
@@ -5686,7 +5689,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -5799,7 +5802,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 25
     },
     {
       "problem_id": 398,
@@ -5822,7 +5825,7 @@
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 400,
@@ -5839,8 +5842,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 +6195,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -6200,7 +6203,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -6363,8 +6366,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 +6499,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 +6756,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -6917,7 +6898,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": 20
     },
     {
       "problem_id": 489,
@@ -7168,7 +7149,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 +7459,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": "",
@@ -7824,7 +7805,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -7999,7 +7980,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -8211,7 +8192,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 +8290,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -8456,7 +8437,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 +8643,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -8831,26 +8812,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",
@@ -9310,8 +9271,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",
@@ -9384,7 +9345,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 +9621,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 706,
@@ -9715,13 +9676,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 +9761,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "06 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/713",
       "formalized": false,
       "formalized_url": "",
@@ -10711,7 +10672,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -10770,8 +10731,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 +11002,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 +11248,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -11317,8 +11278,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": [
@@ -12264,7 +12225,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 +12287,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -12480,7 +12441,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,
@@ -12944,7 +12905,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 975,
@@ -13098,7 +13059,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -13183,7 +13144,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 995,
@@ -13246,7 +13207,7 @@
       "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": 1002,
@@ -13490,12 +13451,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 +13465,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1032,
@@ -13585,7 +13546,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 +13567,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -13626,7 +13587,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -13647,15 +13608,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": 37
     },
     {
       "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 +13628,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1049,
@@ -13687,7 +13648,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 +14048,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -14362,7 +14323,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -14403,7 +14364,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,
@@ -14605,7 +14566,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -14728,7 +14689,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1131,
@@ -14770,7 +14731,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -14904,7 +14865,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -14919,7 +14880,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 +14888,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -15012,29 +14973,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 +15055,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -15456,8 +15394,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 +15408,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -15498,8 +15436,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 +15450,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 +15494,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..9c77e6d 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-03-26T06:41:23Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "171716cab9853224a2367a87091d6cb6a953c3ea1c9801050ed043514d81641d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "492 solved out of 1183 shown",
+      "solved": 492,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 1179,
+    "total": 1183,
     "open": 691,
-    "closed": 488,
+    "closed": 492,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 9,
-      "DISPROVED": 76,
-      "DISPROVED (LEAN)": 40,
-      "FALSIFIABLE": 29,
+      "DISPROVED": 74,
+      "DISPROVED (LEAN)": 42,
+      "FALSIFIABLE": 25,
       "INDEPENDENT": 3,
-      "NOT DISPROVABLE": 2,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 4,
-      "OPEN": 645,
-      "PROVED": 239,
-      "PROVED (LEAN)": 63,
-      "SOLVED": 52,
-      "SOLVED (LEAN)": 10,
+      "OPEN": 647,
+      "PROVED": 238,
+      "PROVED (LEAN)": 68,
+      "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": "",
@@ -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,
@@ -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,
@@ -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,
@@ -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,
@@ -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,
@@ -9592,7 +9599,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -9770,7 +9777,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 25
     },
     {
       "problem_id": 397,
@@ -9814,7 +9821,7 @@
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 399,
@@ -9852,8 +9859,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 +10361,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -10362,7 +10369,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -10814,8 +10821,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 +11062,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 +11079,7 @@
         "https://oeis.org/A391668"
       ],
       "comments_problem_id": 457,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 458,
@@ -11102,8 +11109,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 +11125,7 @@
         "https://oeis.org/A289280"
       ],
       "comments_problem_id": 459,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 460,
@@ -11456,7 +11463,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -11744,7 +11751,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": 20
     },
     {
       "problem_id": 489,
@@ -11865,7 +11872,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 +12350,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 +12831,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/540",
       "formalized": false,
       "formalized_url": "",
@@ -12990,12 +12997,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": "",
@@ -13487,7 +13494,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -13743,7 +13750,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -14061,7 +14068,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 +14187,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -14450,7 +14457,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 +14786,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -15119,22 +15126,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}$?",
       "tags": [
         "number theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 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": 26
     },
     {
       "problem_id": 651,
@@ -15823,8 +15832,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",
@@ -15897,7 +15906,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 +16287,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 705,
@@ -16375,13 +16384,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 +16469,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 +16613,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 +16663,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 722,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 723,
@@ -16784,7 +16793,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,
@@ -17354,8 +17363,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 +17377,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 756,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 757,
@@ -17968,20 +17977,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 +18482,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -18532,8 +18541,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 +19025,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 +19294,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 +19415,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -19436,8 +19445,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": [
@@ -20397,7 +20406,7 @@
       "tags": [
         "graph theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/900",
       "formalized": false,
       "formalized_url": "",
@@ -20694,7 +20703,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 914,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 915,
@@ -20883,7 +20892,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 923,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 924,
@@ -21047,7 +21056,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 +21118,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -21307,7 +21316,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,
@@ -21942,7 +21951,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 974,
@@ -22203,7 +22212,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -22368,7 +22377,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 994,
@@ -22452,7 +22461,7 @@
       "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 +22732,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1010,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1011,
@@ -23131,12 +23140,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 +23154,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1031,
@@ -23306,7 +23315,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 +23336,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -23347,7 +23356,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -23368,7 +23377,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": 37
     },
     {
       "problem_id": 1042,
@@ -23435,8 +23444,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 +23457,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1046,
@@ -23528,7 +23537,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 +24083,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -24516,7 +24525,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -24557,7 +24566,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,
@@ -24841,7 +24850,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -25066,7 +25075,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1121,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 1122,
@@ -25086,7 +25095,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1123,
@@ -25100,7 +25109,7 @@
       "tags": [
         "algebra"
       ],
-      "last_edited": "31 December 2025",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1123",
       "formalized": false,
       "formalized_url": "",
@@ -25294,7 +25303,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -25490,7 +25499,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -25505,7 +25514,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 +25522,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -25622,16 +25631,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 +25649,7 @@
         "https://oeis.org/A393168"
       ],
       "comments_problem_id": 1148,
-      "comments_count": 6
+      "comments_count": 26
     },
     {
       "problem_id": 1149,
@@ -25744,7 +25753,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -26163,8 +26172,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 +26186,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -26205,8 +26214,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 +26228,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 +26293,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..1dca35e 100644
--- a/packs/erdos-open-problems/data/erdos_problems.closed.json
+++ b/packs/erdos-open-problems/data/erdos_problems.closed.json
@@ -2,32 +2,32 @@
   "schema_version": "1.0.0",
   "subset": "closed",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-03-26T06:41:23Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "171716cab9853224a2367a87091d6cb6a953c3ea1c9801050ed043514d81641d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "492 solved out of 1183 shown",
+      "solved": 492,
+      "shown": 1183
     }
   },
   "summary": {
-    "total": 488,
+    "total": 492,
     "open": 0,
-    "closed": 488,
+    "closed": 492,
     "unknown": 0,
     "status_label_counts": {
       "DECIDABLE": 7,
-      "DISPROVED": 76,
-      "DISPROVED (LEAN)": 39,
+      "DISPROVED": 74,
+      "DISPROVED (LEAN)": 41,
       "INDEPENDENT": 3,
       "NOT PROVABLE": 1,
-      "PROVED": 237,
-      "PROVED (LEAN)": 63,
-      "SOLVED": 52,
-      "SOLVED (LEAN)": 10
+      "PROVED": 236,
+      "PROVED (LEAN)": 68,
+      "SOLVED": 51,
+      "SOLVED (LEAN)": 11
     }
   },
   "problem_ids": [
@@ -222,6 +222,7 @@
     448,
     449,
     453,
+    457,
     459,
     464,
     465,
@@ -305,6 +306,7 @@
     646,
     648,
     649,
+    650,
     651,
     652,
     656,
@@ -513,12 +515,14 @@
     1136,
     1140,
     1147,
+    1148,
     1149,
     1161,
     1164,
     1165,
     1166,
-    1179
+    1179,
+    1180
   ],
   "problems": [
     {
@@ -670,7 +674,7 @@
         "graph theory",
         "chromatic number"
       ],
-      "last_edited": "23 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/19",
       "formalized": false,
       "formalized_url": "",
@@ -2024,12 +2028,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 +2215,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 +2229,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 +2487,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 221,
-      "comments_count": 2
+      "comments_count": 4
     },
     {
       "problem_id": 223,
@@ -2538,7 +2542,7 @@
       "tags": [
         "analysis"
       ],
-      "last_edited": "01 February 2026",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/225",
       "formalized": false,
       "formalized_url": "",
@@ -3448,7 +3452,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 314,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 315,
@@ -3724,7 +3728,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 +3795,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 +3808,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 363,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 370,
@@ -4584,13 +4588,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 +4631,7 @@
         "https://oeis.org/A289280"
       ],
       "comments_problem_id": 459,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 464,
@@ -4954,7 +4980,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 +5453,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "28 December 2025",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/540",
       "formalized": false,
       "formalized_url": "",
@@ -6313,6 +6339,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)\\ll m^{1/2}$?",
+      "tags": [
+        "number theory"
+      ],
+      "last_edited": "07 March 2026",
+      "latex_path": "/latex/650",
+      "formalized": false,
+      "formalized_url": "",
+      "oeis_urls": [
+        "https://oeis.org/A027434"
+      ],
+      "comments_problem_id": 650,
+      "comments_count": 26
+    },
     {
       "problem_id": 651,
       "problem_url": "/651",
@@ -6782,7 +6830,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 +6880,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 722,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 728,
@@ -6853,7 +6901,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 +7239,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 +7253,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 756,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 758,
@@ -7528,20 +7576,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 +8193,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,
@@ -8455,7 +8503,7 @@
       "tags": [
         "graph theory"
       ],
-      "last_edited": "",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/900",
       "formalized": false,
       "formalized_url": "",
@@ -8622,7 +8670,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 914,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 915,
@@ -8727,7 +8775,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 923,
-      "comments_count": 1
+      "comments_count": 0
     },
     {
       "problem_id": 924,
@@ -9418,7 +9466,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1010,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1012,
@@ -10384,7 +10432,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1121,
-      "comments_count": 0
+      "comments_count": 2
     },
     {
       "problem_id": 1123,
@@ -10398,7 +10446,7 @@
       "tags": [
         "algebra"
       ],
-      "last_edited": "31 December 2025",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/1123",
       "formalized": false,
       "formalized_url": "",
@@ -10635,6 +10683,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 +10826,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..c1b8dc2 100644
--- a/packs/erdos-open-problems/data/erdos_problems.open.json
+++ b/packs/erdos-open-problems/data/erdos_problems.open.json
@@ -2,15 +2,15 @@
   "schema_version": "1.0.0",
   "subset": "open",
   "active_status": "open",
-  "generated_at_utc": "2026-03-05T15:52:31Z",
+  "generated_at_utc": "2026-03-26T06:41:23Z",
   "source": {
     "site": "erdosproblems.com",
     "url": "https://erdosproblems.com/range/1-end",
-    "source_sha256": "72366d21b9530355396bef95b3ead90176a9c634b7ecd68fd30c85bad703a0c1",
+    "source_sha256": "171716cab9853224a2367a87091d6cb6a953c3ea1c9801050ed043514d81641d",
     "solve_count": {
-      "raw": "488 solved out of 1179 shown",
-      "solved": 488,
-      "shown": 1179
+      "raw": "492 solved out of 1183 shown",
+      "solved": 492,
+      "shown": 1183
     }
   },
   "summary": {
@@ -21,10 +21,10 @@
     "status_label_counts": {
       "DECIDABLE": 2,
       "DISPROVED (LEAN)": 1,
-      "FALSIFIABLE": 29,
-      "NOT DISPROVABLE": 2,
+      "FALSIFIABLE": 25,
+      "NOT DISPROVABLE": 4,
       "NOT PROVABLE": 3,
-      "OPEN": 645,
+      "OPEN": 647,
       "PROVED": 2,
       "VERIFIABLE": 7
     }
@@ -295,7 +295,6 @@
     454,
     455,
     456,
-    457,
     458,
     460,
     461,
@@ -405,7 +404,6 @@
     643,
     644,
     647,
-    650,
     653,
     654,
     655,
@@ -695,7 +693,6 @@
     1144,
     1145,
     1146,
-    1148,
     1150,
     1151,
     1152,
@@ -720,7 +717,10 @@
     1175,
     1176,
     1177,
-    1178
+    1178,
+    1181,
+    1182,
+    1183
   ],
   "problems": [
     {
@@ -870,8 +870,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 +993,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 +1013,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 +1063,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 +1152,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 +1346,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 +1388,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 +1747,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 +1878,7 @@
         "https://oeis.org/A186704"
       ],
       "comments_problem_id": 91,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 92,
@@ -2105,7 +2105,7 @@
       "tags": [
         "geometry"
       ],
-      "last_edited": "",
+      "last_edited": "06 March 2026",
       "latex_path": "/latex/106",
       "formalized": false,
       "formalized_url": "",
@@ -2281,7 +2281,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,
@@ -2826,13 +2826,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 +2919,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 +2961,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 +3102,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 176,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 177,
@@ -3205,11 +3205,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 +3289,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 +3693,7 @@
         "https://oeis.org/A387704"
       ],
       "comments_problem_id": 241,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 242,
@@ -3744,7 +3744,7 @@
         "https://oeis.org/A000058"
       ],
       "comments_problem_id": 243,
-      "comments_count": 6
+      "comments_count": 7
     },
     {
       "problem_id": 244,
@@ -3872,8 +3872,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 +3952,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 +4162,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,
@@ -4723,8 +4723,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 +4769,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 +4790,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,
@@ -4893,7 +4893,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 +5022,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 +5114,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,
@@ -5686,7 +5689,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 388,
-      "comments_count": 5
+      "comments_count": 10
     },
     {
       "problem_id": 389,
@@ -5799,7 +5802,7 @@
         "https://oeis.org/A375077"
       ],
       "comments_problem_id": 396,
-      "comments_count": 1
+      "comments_count": 25
     },
     {
       "problem_id": 398,
@@ -5822,7 +5825,7 @@
         "https://oeis.org/A146968"
       ],
       "comments_problem_id": 398,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 400,
@@ -5839,8 +5842,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 +6195,7 @@
       "tags": [
         "number theory"
       ],
-      "last_edited": "16 January 2026",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/423",
       "formalized": false,
       "formalized_url": "",
@@ -6200,7 +6203,7 @@
         "https://oeis.org/A005243"
       ],
       "comments_problem_id": 423,
-      "comments_count": 18
+      "comments_count": 38
     },
     {
       "problem_id": 424,
@@ -6363,8 +6366,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 +6499,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 +6756,7 @@
         "number theory",
         "additive combinatorics"
       ],
-      "last_edited": "",
+      "last_edited": "05 March 2026",
       "latex_path": "/latex/475",
       "formalized": false,
       "formalized_url": "",
@@ -6917,7 +6898,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": 20
     },
     {
       "problem_id": 489,
@@ -7168,7 +7149,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 +7459,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": "",
@@ -7824,7 +7805,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "18 January 2026",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/571",
       "formalized": false,
       "formalized_url": "",
@@ -7999,7 +7980,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 583,
-      "comments_count": 1
+      "comments_count": 3
     },
     {
       "problem_id": 584,
@@ -8211,7 +8192,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 +8290,7 @@
         "geometry",
         "distances"
       ],
-      "last_edited": "15 October 2025",
+      "last_edited": "23 March 2026",
       "latex_path": "/latex/604",
       "formalized": false,
       "formalized_url": "",
@@ -8456,7 +8437,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 +8643,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 633,
-      "comments_count": 2
+      "comments_count": 5
     },
     {
       "problem_id": 634,
@@ -8831,26 +8812,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",
@@ -9310,8 +9271,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",
@@ -9384,7 +9345,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 +9621,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 704,
-      "comments_count": 1
+      "comments_count": 4
     },
     {
       "problem_id": 706,
@@ -9715,13 +9676,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 +9761,7 @@
         "graph theory",
         "turan number"
       ],
-      "last_edited": "06 October 2025",
+      "last_edited": "07 March 2026",
       "latex_path": "/latex/713",
       "formalized": false,
       "formalized_url": "",
@@ -10711,7 +10672,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 809,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 810,
@@ -10770,8 +10731,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 +11002,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 +11248,7 @@
         "https://oeis.org/A390769"
       ],
       "comments_problem_id": 853,
-      "comments_count": 2
+      "comments_count": 3
     },
     {
       "problem_id": 854,
@@ -11317,8 +11278,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": [
@@ -12264,7 +12225,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 +12287,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 934,
-      "comments_count": 0
+      "comments_count": 3
     },
     {
       "problem_id": 935,
@@ -12480,7 +12441,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,
@@ -12944,7 +12905,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 973,
-      "comments_count": 7
+      "comments_count": 6
     },
     {
       "problem_id": 975,
@@ -13098,7 +13059,7 @@
         "https://oeis.org/A219429"
       ],
       "comments_problem_id": 985,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 986,
@@ -13183,7 +13144,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 993,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 995,
@@ -13246,7 +13207,7 @@
       "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": 1002,
@@ -13490,12 +13451,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 +13465,7 @@
         "https://oeis.org/A059442"
       ],
       "comments_problem_id": 1030,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1032,
@@ -13585,7 +13546,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 +13567,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1039,
-      "comments_count": 1
+      "comments_count": 9
     },
     {
       "problem_id": 1040,
@@ -13626,7 +13587,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1040,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1041,
@@ -13647,15 +13608,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": 37
     },
     {
       "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 +13628,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1045,
-      "comments_count": 43
+      "comments_count": 45
     },
     {
       "problem_id": 1049,
@@ -13687,7 +13648,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 +14048,7 @@
         "https://oeis.org/A064164"
       ],
       "comments_problem_id": 1074,
-      "comments_count": 3
+      "comments_count": 5
     },
     {
       "problem_id": 1075,
@@ -14362,7 +14323,7 @@
         "https://oeis.org/A003458"
       ],
       "comments_problem_id": 1095,
-      "comments_count": 6
+      "comments_count": 8
     },
     {
       "problem_id": 1096,
@@ -14403,7 +14364,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,
@@ -14605,7 +14566,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1110,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1111,
@@ -14728,7 +14689,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1122,
-      "comments_count": 0
+      "comments_count": 1
     },
     {
       "problem_id": 1131,
@@ -14770,7 +14731,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1132,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1133,
@@ -14904,7 +14865,7 @@
         "https://oeis.org/A214583"
       ],
       "comments_problem_id": 1141,
-      "comments_count": 5
+      "comments_count": 6
     },
     {
       "problem_id": 1142,
@@ -14919,7 +14880,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 +14888,7 @@
         "https://oeis.org/A039669"
       ],
       "comments_problem_id": 1142,
-      "comments_count": 3
+      "comments_count": 4
     },
     {
       "problem_id": 1143,
@@ -15012,29 +14973,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 +15055,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1153,
-      "comments_count": 7
+      "comments_count": 10
     },
     {
       "problem_id": 1154,
@@ -15456,8 +15394,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 +15408,7 @@
       "formalized_url": "",
       "oeis_urls": [],
       "comments_problem_id": 1174,
-      "comments_count": 1
+      "comments_count": 2
     },
     {
       "problem_id": 1175,
@@ -15498,8 +15436,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 +15450,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 +15494,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
     }
   ]
 }