Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean e erdosproblems.com 16 mathfan 11 months ago 2 comments
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT a arxiv.org 5 mathfan 1 year ago 0 comments
Sebastien Bubeck: Another twist in the Erdős problems story t twitter.com 5 mathfan 1 year ago 1 comments
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT m mathstodon.xyz 5 mathfan 1 year ago 1 comments
We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT b borisalexeev.com 17 mathfan 1 year ago 4 comments
You Want Voting Districts to Be Only 4% Pretty [video] y youtube.com 4 mathfan 3 years ago 0 comments