Matroids and Computation
Computational tools will advance progress in matroid theory, giving us new ways to find counterexamples, detect patterns in large datasets, and certify proofs.
Matroids capture the essence of "independence" in mathematics. They show up in graphs, vector configurations, matchings, field extensions, and convex optimization, which puts matroid theory at the intersection of algebraic geometry, topology, convex geometry, discrete optimization, and probability. The field has moved quickly in recent years, driven by the Hodge theory of matroids and by advances in probabilistic and extremal combinatorics. Computational tools are increasingly part of that progress. For example, counterexamples to White's conjecture were recently found by two separate methods, one with a SAT solver and one with a large language model.
This workshop will bring together structural and extremal matroid theorists, combinatorial algebraic geometers, software developers and machine-learning practitioners to use computer-aided reasoning to:
- find counterexamples and extremal examples;
- generate large, feature-rich datasets of matroids and detect patterns in them;
- train models that generate matroids with prescribed features or predict matroid invariants;
- settle open problems and find new directions suggested by the data; and
- formalize matroid results in Lean and produce machine-checkable certificates for computational steps in proofs.
Expected outcomes include shared, documented workflows for these tools, efficient methods for computing hard matroid invariants that will be contributed back to SageMath, OSCAR and Macaulay2, and a centralized, queryable matroid database modeled on the LMFDB. The database will build on a recent enumeration of about 3 trillion matroids.