erdos

Composable mathematics tools for agents

Modular and modern graph-theory algorithms framework in Java

A toolkit for AI agents to explore and attempt Erdős's 1,179 unsolved mathematical problems

Certified unit-distance point sets and graphs for discrete geometry in Rust.

CLI and workspace for Paul Erdos problems.

Computational evidence isolating the log(n) spreadness artifact in the Erdős k=3 Sunflower Conjecture via bitmask-accelerated Simulated Annealing.

Independent Python reproduction of the 2026 OpenAI/Sawin disproof of the Erdős unit-distance conjecture. mpmath-200-bit verbatim match (0.01% rel.err) to equation (2.2) of the remarks PDF. MIT, NumPy + mpmath only.

Erdos problem 1191 and Sidon sets: Lean 4 formulations, supporting lemmas, finite formalizations, and computational experiments. Research in progress.

Sundai Hack 142: Erdős 3 research, 14 Lean-checked elementary theorems, and an interactive proof lab. Full conjecture remains open.

A tighter proven upper bound for the Erdős minimum overlap constant, with machine-verifiable certificates (note + code + certs).

AI trying to tackle erdos problems

Proof package for a certified pointwise lower bound in the Erdős unit-distance problem

Erdos-SDSLabs solutions using Python (Mostly)

Erdős unit distance problem: disproof and exposition. Study project on the May 2026 AI-solved open problem.

Computational experiments for Erdős-style combinatorial conjectures

Solutions of various online judges

Royce — bioinformatics (cfDNA cancer detection, mRNA × AI tooling) and verified math in Lean 4 (Navier–Stokes + Erdős #125). HKT.

Reproducible generator for Erdős problem LaTeX, metadata, status, formalization, and AI provenance

Computer-assisted proof and reproducibility package for Erdős Problem 848, with exact certificates and separately implemented checkers.

Erdős problem 142 research notebook — OPEN (single final obstruction). Audits, verifiers, roadmap. © Mangesh Raut