Search results

residueAux is a partial def, blocking induction on residue

Status: Open.

#4413 In google-deepmind/formal-conjectures;

· ChakshuGupta13 opened on Jul 9, 2026

Autoformalization error on auto_oeis: a089026 in 7406_a8289e8e.lean encodes A000188, not A089026 (statement false at n=4)

Status: Open.

#4410 In google-deepmind/formal-conjectures;

· Harmenszoon opened on Jul 8, 2026

Add IMO 2013 Problem 6 (beautiful labellings count) as a research-solved combinatorics statement

Status: Open.

#4408 In google-deepmind/formal-conjectures;

· him1411 opened on Jul 8, 2026

Bounds on clique-detecting circuits, in *tiny* graphs

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

Status: Open.

#4404 In google-deepmind/formal-conjectures;

· joshtburdick opened on Jul 6, 2026

Tracking: tooling to reduce maintainer review cycles

Status: Open.

#4394 In google-deepmind/formal-conjectures;

· williamjblair opened on Jul 4, 2026

Erdős 522: h_unif is unsatisfiable by measurable coefficients — the defaulted volume reference measure degenerates on the null set {-1, 1}

Status: Open.

#4386 In google-deepmind/formal-conjectures;

· widefox opened on Jul 3, 2026

Erdős Problem 865: status mismatch (repo=open, 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.

#4373 In google-deepmind/formal-conjectures;

· github-actions opened on Jul 2, 2026

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

erdos-status-sync

Status: Open.

#4358 In google-deepmind/formal-conjectures;

· github-actions opened on Jun 29, 2026

verso for FormalConjecturesForMathlib

documentationImprovements or additions to documentationImprovements or additions to documentation

website

Status: Open.

#4306 In google-deepmind/formal-conjectures;

· mo271 opened on Jun 23, 2026

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

erdos-status-sync

Status: Open.

#4298 In google-deepmind/formal-conjectures;

· github-actions opened on Jun 22, 2026

Formalize and refute TxGraffiti Conjecture 4 (saturation number vs. harmonic index)

Status: Open.

#4277 In google-deepmind/formal-conjectures;

· ChakshuGupta13 opened on Jun 16, 2026

Synthetic formulations

Status: Open.

#4261 In google-deepmind/formal-conjectures;

· qrdlgit opened on Jun 14, 2026