Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claims
2026_04_20_chojecki: Chojecki, working with GPT-5.4 Pro and GPT-5.5 Pro, claims that the number of roots in the closed unit disk is n over two plus a power saving almost surely; two notes on the site's thread, revised after a reader found an error.
2026_04_28_kwon_zou: Kwon and Zou, working with ChatGPT 5.5 Pro, claim that the number of roots in the closed unit disk is n over two up to n to the seven eighths plus delta almost surely; a note in a public repository, no review.
2026_07_23_snyder: A Lean 4 theorem credited to Colin Snyder of Star Fleet Math states that the number of roots in the closed unit disk divided by n over two tends to one almost surely for independent fair signs; lean-proofs repository, no write-up.
2026_09_25_kawada: Kawada claims an almost-sure law for the number of roots in disks of radius one plus x over n, whose case x equal to zero is the asked convergence, with a Lean 4 formalization; a Zenodo preprint and a claim on the site's tab.
2026_09_25_kitamura: Kitamura, with AI assistance, gives a Lean 4 proof that the number of roots in the closed unit disk divided by n over two tends to one almost surely, for sign and for zero-one coefficients; linked by formal-conjectures, not audited.