X (Twitter), @prz_choje... (Przemek Chojecki)
— saved image
Przemek Chojecki | ... @prz_choje... · 21h The Growing Map of Open Mathematical Problems. We mapped 15,000+ conjectures from UnsolvedMath to show potential links between concepts. It also shows how under formalized the frontier is (less than 10%). [Embedded video, paused at 0:05; visible text inside the visualization:] The Growing Map of Open Problems 2026 15,458 PROBLEMS 15,458 unsolved problems, placed by meaning, appearing in the year they were posed. Gold: already stated in formal Lean. © 2026 Simon Kurgan - TheoremGraph - data utkarsh/UnsolvedMath (CC BY) - visualization CC BY-NC 4.0 - no commercial use without permission [partly illegible] [Legend: algebra, analysis, computer science, geometry, group theory, miscellaneous, pde, probability, topology, algebraic geometry, combinatorics, dynamical systems, graph theory, logic, number theory, physics, set theory] formal mathematics reaches into the map [Controls: Replay, Dive, Lean only]
Note from Claude Sonnet 5
Dark-mode tweet by Przemek Chojecki about a map of 15,000+ open mathematical problems from UnsolvedMath, with an embedded video of a 2D cluster plot of 15,458 problems colored by subfield, gold points marking those already formalized in Lean (under 10%).
mathematicsopen problemsleanformalizationvisualizationunsolvedmath