All issues

Search results

ErdosProblems/945: formal_proof link available for erdos_945.variants.equivalence

Status: Open.

#5089 In google-deepmind/formal-conjectures;

· jkleid opened on Aug 21, 2026

distinctDistancesFrom counts the self-distance 0

Status: Open.

#5064 In google-deepmind/formal-conjectures;

· theebayuser opened on Aug 19, 2026

Erdős Problem 394: lower_bound has the sides of ≫ swapped (states an upper bound instead of the lower bound)

misformalization

Status: Open.

#5062 In google-deepmind/formal-conjectures;

· KitaKen1 opened on Aug 19, 2026

Erdős 243: record Koizumi's Sylvester and Millin rigidity corollaries

Status: Open.

#5058 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Erdős 1049: record the Bundschuh–Väänänen criterion for non-integer rational bases

Status: Open.

#5056 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Erdős 257: add settled support families and the structure of the value space

Status: Open.

#5054 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Erdős 68: add the cofinal strict-successor divisibility reformulation

Status: Open.

#5053 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Erdős 269: add the three-prime smooth-prefix LCM identity

Status: Open.

#5051 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Erdős 251: add the prime-gap summation-by-parts identity and irrationality transfer

Status: Open.

#5052 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 19, 2026

Formal proofs for erdos_885 variants k_eq_2 and k_eq_3

Status: Open.

#5050 In google-deepmind/formal-conjectures;

· Alexispap opened on Aug 19, 2026

Erdős 1041: add a solved unit-disc root-retention variant

Status: Open.

#5048 In google-deepmind/formal-conjectures;

· wcook04 opened on Aug 18, 2026

Erdős Problem 399: status mismatch (repo=solved, erdosproblems.com=formally solved)

erdos-status-sync

formalisation exists elsewhereIndicates that a formalisation of the problem exists and should be portedIndicates that a formalisation of the problem exists and should be ported

Status: Open.

#5046 In google-deepmind/formal-conjectures;

· github-actions opened on Aug 18, 2026