🦞🌯 Lobster Roll

Stories by mathfan

Asymptotically optimal approximate Hadamard matrices (arxiv.org)
HN 19 pts 2 comments by mathfan Nov 19, 2025 thread
We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT (borisalexeev.com)
HN 17 pts 4 comments by mathfan Oct 21, 2025 AI / Machine Learning thread
Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean (erdosproblems.com)
HN 16 pts 2 comments by mathfan Nov 29, 2025 Science / Math / Physics thread
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT (arxiv.org)
HN 5 pts 0 comments by mathfan Oct 23, 2025 AI / Machine LearningProgramming (General) thread
Sebastien Bubeck: Another twist in the Erdős problems story (twitter.com)
HN 5 pts 1 comments by mathfan Oct 23, 2025 thread
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT (mathstodon.xyz)
HN 5 pts 1 comments by mathfan Oct 22, 2025 AI / Machine LearningProgramming (General) thread