Grateful to have been part of this project and to see @nasqret herding a bunch of stochastic parrots excited to write Lean proofs.
Major announcement in mathematical formalization!
Finally, after 3 months of very intensive, nonstop work by several AI agents (Codex and Claude Code), we have settled a classification of ALL 15,973 semigroups of order 6. Every one of the 15,969 that has a finite basis now has it written down explicitly, and the remaining 4 are proved to have none at all.
The whole list of bases is produced for the first time in history. Until now, for most of these semigroups, mathematicians only knew that a basis exists; nobody had ever written one down. The formalization in Lean, orchestrated with a multi-agent approach, reached more than 5 MILLION lines of verified Lean code, one of the largest auto-formalization projects to date.
It's been an amazing joint work with @JanotaMikolas and @Jan_Hula, accompanied by senior experts in semigroup theory, João Araújo and Edmond W. H. Lee.
Our paper describing this project, "Proving at Scale for Universal Algebra", has been accepted at the MATH-AI workshop, NeurIPS 2026!
When we launched this project, we were a bit pessimistic: producing proofs for 15,973 semigroups seemed out of scope for the current technology. But with a careful setup (agents communicating through a mailbox we arranged, orchestrating the effort with a custom method of bootstrapping and auto-research), it has finally come to the finish line. The last 390 semigroups took 23 more days. The very last one needed a whole structural analysis before its proof could even be written.
Jan Hůla retweeted
Major announcement in mathematical formalization!
Finally, after 3 months of very intensive, nonstop work by several AI agents (Codex and Claude Code), we have settled a classification of ALL 15,973 semigroups of order 6. Every one of the 15,969 that has a finite basis now has it written down explicitly, and the remaining 4 are proved to have none at all.
The whole list of bases is produced for the first time in history. Until now, for most of these semigroups, mathematicians only knew that a basis exists; nobody had ever written one down. The formalization in Lean, orchestrated with a multi-agent approach, reached more than 5 MILLION lines of verified Lean code, one of the largest auto-formalization projects to date.
It's been an amazing joint work with @JanotaMikolas and @Jan_Hula, accompanied by senior experts in semigroup theory, João Araújo and Edmond W. H. Lee.
Our paper describing this project, "Proving at Scale for Universal Algebra", has been accepted at the MATH-AI workshop, NeurIPS 2026!
When we launched this project, we were a bit pessimistic: producing proofs for 15,973 semigroups seemed out of scope for the current technology. But with a careful setup (agents communicating through a mailbox we arranged, orchestrating the effort with a custom method of bootstrapping and auto-research), it has finally come to the finish line. The last 390 semigroups took 23 more days. The very last one needed a whole structural analysis before its proof could even be written.
Jan Hůla retweeted
We’re excited to announce DiG-bench, a new benchmark for discovery!
Over the last few weeks we’ve been testing frontier AI models on our novel discovery games and seeing how they score. Each game is a text-based environment, so they probe discovery capabilities in the natural domain of language models, rather than requiring additional, potentially confounding, visual understanding.
TL;DR frontier models have improved a lot over the last few months. But they are still stumped by some surprisingly simple problems, even in their native text domain.
With
@cocosci_lab (@Princeton) @MITCoCoSci (@MIT) @SchmidhuberAI (@KAUST_News) @misovalko (@Inria) @tri_dao (@PrincetonCS) @RMBattleday @zebkDotCom @FraserGreenlee @akaijsa @ClareMaguire @TimMuller1 @kubicek_ales @physicscat0x7d @SukritSumant @thoughtchannel_
(1/5)
Jan Hůla retweeted
Our groups is opening a PostDoc position. We are seeking candidates in theorem proving, SMT, and formal verification.
linkedin.com/jobs/view/42907…
Jan Hůla retweeted
❗Reminder – July 10 at CIIRC: Prague Synapse, the first Prague-based workshop on neural networks and reasoning.
🎫 Free entry, limited to 50 seats.
Register at 👉 praguesynapse.cz/
@Ostravska_uni
@IDEAS_NCBR
@muni_cz
@epfl_en
@UniofOxford
@GoogleDeepMind
@ethzurich
Jan Hůla retweeted
We are looking for a Postdoc to join our team in Prague, with a focus on theorem proving, SMT (Satisfiability Modulo Theories), or formal methods.
Jan Hůla retweeted
First call for papers for the workshop Pragmatics of SAT (PoS). Since this year SAT is colocated with CP, the workshop also reflects that. pragmaticsofsat.org/2025/
Jan Hůla retweeted
We are announcing the first call for papers of SC-Square 2025, the 10th International Workshop on Satisfiability Checking and Symbolic Computation, which will take place on August 2, 2025, Stuttgart Germany as a satellite event of CADE. For more, see sc-square.org/CSA/workshop10…
Jan Hůla retweeted
AE Global Summit on Open Problems for AI (London, Oct 23-24): Final Line-up and Reduced Ticket Prices: algopreneurship.org
It’s a pleasure to announce the final program for our upcoming Summit on Open Problems for AI in London. We have what might actually be the best 2-day line-up of UK experts in AI research and application I’ve ever seen!
On Algorithms Day (Oct 23rd), we have leading keynotes from @GoogleDeepMind, @ucl, @MSFTResearch, @imperialcollege & @VERSESAI.
- In the morning we have a panel on new types of institutions for AI research, featuring leaders from @KingsCollegeLon, @turinginst, @ARIA_research, Cambridge Consultants & @InstituteGC.
- In the afternoon we have a panel on Current Challenges for AI/ML Algorithms, with researchers from @UniofOxford, @GoogleDeepMind, @Cambridge_Uni, @AIatMeta & @xtxmarkets.
On Applications Day (Oct 24th), we’ll begin with keynotes from @OpenAI and @responsibleaiuk, and then hear from @Spotify, Academy, JAAQ., Akord AI, Boon io, @imperialcollege & @Basecamp_Res.
- Breakout rooms by @FLFDevNetwork, No 10 Downing Street Data Science Team, @InstituteGC, Zeki Data, @joinef & @OctopusVentures.
- Panel on AI & Education, featuring @RaspberryPi_org, Inversity, @memrise, @microbit_edu & @University of Cambridge
Panel on AI & Medicine, featuring @KingsCollegeLon, @QMUL, @DecorteFuture & @redalpine.
Come and join the debate!
xitter.cf/RMBattleday/status/183…
For AI students, researchers & entrepreneurs in London:
algopreneurship.org
Join our Autumn Summit on Open Problems in AI!
What are the next set of challenges in AI research? What are key opportunities for application?
Researchers and leaders from the UK’s top AI institutions and funders.
With @jcrwhittington
Jan Hůla retweeted
Sharpen your pencils! FMCAD 2024 is taking place in Prague fmcad.org/FMCAD24/cfp/
Jan Hůla retweeted
We are opening a position for a Postdoc and PhD candidates interested in SMT, automated reasoning, and Formal Methods. More here: people.ciirc.cvut.cz/~janotm…
Tento týden probíhá festival Brain Awareness Week, tak jsem za Ostravskou taky něco natočil: youtube.com/watch?v=H2l6-cm9…
For my English-speaking friends: I'm posting a video which I shot at my uni as part of Brain Awareness Week festival. Unfortunately, it's only in Czech.
Jan Hůla retweeted
Very cool: same speed, different fields of view.
Your 🧠 uses objects’ velocity relative to each other to form a perception of speed.
xitter.cf/Unexplained/status/122…
Jan Hůla retweeted
Amazing: a trail of termites (up) and a trail of ants (down), both protected by a row of their soldiers in a stand-off, without fighting.
from @mehdi_moussaid
Jan Hůla retweeted
A ball rolling on the surface of the Penrose triangle, a 3D object that is impossible to realize in ordinary Euclidean space. en.wikipedia.org/wiki/Penros…
Jan Hůla retweeted
Woah! pyforest lazy-imports all popular Python Data Science libraries with a single line of code!
pip install pyforest 👏
github.com/8080labs/pyforest
Jan Hůla retweeted
The Czech Play That Gave Us the Word ‘Robot’. Interesting context. thereader.mitpress.mit.edu/o…
