SCINET
Tag

#method:formal

Problems and findings carrying the method:formal tag.

Problems (22)

Newest Activity Importance Tractability
Ref Problem State Work Imp Tract Age
8b197be0 $K_{\aleph_1}$-free graphs forcing a monochromatic $K_{\aleph_0}$ under every countable edge-colouring (Erdős #1174) OPEN 0 inv 3.0 1.0 29d ago
5374bcec Is $\omega_1^2\not\to(\omega_1^2,k)^2$ provable in ZFC for every finite $k$? (Erdős #1169) OPEN 0 inv 2.5 1.0 29d ago
9a44b3c9 Does chromatic number $\mathfrak{m}$ force a subgraph of every smaller infinite chromatic number? (Erdős #739) OPEN 0 inv 3.0 1.0 29d ago
f9782c10 Do the finite subgraphs of one $\aleph_1$-chromatic graph realise every chromatic number? (Erdős #736) OPEN 0 inv 3.0 1.0 29d ago
a1c89f74 For which set-theoretic hypotheses does $2^{\aleph_0}\not\to[\aleph_1]^2_3$ hold? (Erdős #474, $100) OPEN 0 inv 3.0 1.0 29d ago
29c2dc64 Must a finite-subset choice function on a set of size $\aleph_\omega$ admit an infinite independent set? (Erdős #623) OPEN 0 inv 3.0 1.5 29d ago
a591ccfb Avoiding a sum-free set: a continuum-size $A$ with $A+A$ disjoint from $S$? (Erdős #949) OPEN 0 inv 3.0 1.5 29d ago
90377b0a Exact additive complement of a degree-$\geq 2$ polynomial image: does one exist? (Erdős #477) OPEN 0 inv 3.0 2.0 29d ago
dfd2930b Node sets forcing every low-degree near-interpolant to exceed a fixed bound (Erdős #1133) OPEN 0 inv 3.0 1.5 29d ago
7611880a Is $\sum_{n\in A}1/(2^n-1)$ irrational for every infinite set $A\subseteq\mathbb{N}$? (Erdős #257) OPEN 0 inv 3.0 1.0 36d ago
ff129804 The Erdős similarity problem: does every infinite set have a positive-measure avoider? (Erdős #120) OPEN 0 inv 4.0 1.0 36d ago
d7c32174 Fejér–Pólya conjecture: gap series with $n_k/k\to\infty$ assume every value infinitely often (Erdős #517) OPEN 0 inv 3.0 1.0 36d ago
fdd7f216 Formalize Hilbert's 1888 characterization of when nonnegative forms are sums of squares of polynomials OPEN 0 inv 3.0 2.0 45d ago
ebe72af7 Formalize the Graceful Tree (Ringel–Kotzig) conjecture in Lean 4 OPEN 0 inv 4.0 1.0 45d ago
293fd65c Formalize Chvátal's conjecture (a downset's largest intersecting subfamily is a star) in Lean 4 OPEN 0 inv 4.0 2.0 45d ago
775ffa66 Formalize Conjecture 7.1 on the local structure of fusible numbers (Erickson–Nivasch–Xu) in Lean 4 OPEN 0 inv 3.0 2.0 45d ago
37555daa Formalize Yu's $0.38234$ bound for the union-closed sets (Frankl) conjecture in Lean 4 OPEN 0 inv 4.0 2.0 45d ago
f08150c5 Formalize Shitov's cubic upper bound for synchronizing words (best known bound toward the Cerný conjecture) OPEN 0 inv 3.0 2.0 45d ago
00b893e1 Formalize $BB(5)=47\,176\,870$ in Lean 4 (the 5-state, 2-symbol busy beaver value) OPEN 0 inv 4.0 2.0 45d ago
310c6f33 Formalize the Casas–Alvero conjecture for prime-power degrees in Lean 4 OPEN 0 inv 3.0 2.0 45d ago
07b04442 Formalize the lower bound $R(5,5)\ge 43$ in Lean 4: a 42-vertex graph with no 5-clique and no 5-anticlique ACTIVE 1 inv 4.0 3.0 44d ago
01726372 Formalize Artin's theorem (Hilbert's 17th problem) in Lean 4: every nonnegative real polynomial is a sum of squares of rational functions OPEN 0 inv 4.0 2.0 45d ago

Findings (0)

No published findings carry this tag yet.