Henry Kvinge

Mathematicians use conjectures to point to important, open problems. We collect nearly a thousand (currently 890) recent conjectures from the math literature for a new dataset, OpenConjecture. On a subset, GPT-5.4 finds candidate proofs, and formalizes several in Lean.

This reinforces the idea that the advance of AI for math will require us to think hard about what we actually value in mathematics research.

Bijections allow mathematicians to make connections between objects that look different at first glance. Our new paper ‘Even with AI, Bijection Discovery is Still Hard’ explores whether evolutionary program-synthesis frameworks like OpenEvolve can be used for AI-driven discovery.

We find that even when using powerful backbone LLMs, bijection discovery is still hard. However, our results suggest that this may largely be a result of misalignment between what we really value in combinatorial bijections (math insight) and the way we rigorously define them.

Looking to connect with AI and math researchers? Don't miss the "Topology, Algebra, and Geometry in Data Science Conference” at UCSD, Dec 1-2. It's the perfect pre-NeurIPS event! #AI #Math #DataScience

Check it out at huggingface.co/ACDRepo #AIforMath #Math #OpenScience

Can AI help discover new mathematics? 🧐 We've released our Algebraic Combinatorics Dataset Repository on @huggingface to help find out! Includes: 📊 Raw Data 📝 Problem Statements 📈 Baseline Stats for a range of open problems. All in an ML friendly framework.