Research initiative
Mantis Discovery
We work in mathematics, machine learning, physics, chemistry and biology. We do our research in Mantis, a knowledge platform built at MIT CSAIL.
Mantis
Mantis puts the papers, code and data behind a project into one shared space, where AI agents work with our researchers. The agents search the literature and run computations. The researchers check what the agents produce and choose which ideas to pursue.
Walkthrough
Our approach
Each project has its own space in Mantis. Everything we write or compute for a project is saved there as a record, which we can search and cite later.
Geometric reasoning
Mantis represents each record as a point in a space with thousands of dimensions and draws the points as a map, so records that say similar things sit close together. We search the map and outline regions of it to compare the records inside.
We can see a project’s whole history at once. Related attempts end up near each other, so it is easy to notice when an idea has been tried before.
The opaque sets space holds 1,433 records, grouped into named clusters. Traceability
Failed attempts stay in the project along with the fixes that followed them. Each record points to the file and lines it came from and stores a hash of that source, and it carries a status such as withdrawn or independently verified.
Anyone can follow how we reached a result, including the approaches that did not work.
This record holds a theorem from an early draft of the Hadwiger paper, kept as history, and points to lines 66 to 71 of its source. Audits
Before a claim goes into a paper, we check it against the records behind it. For our Hadwiger paper, an audit found that an early draft used an inequality in the wrong direction. Later rewrites brought the claimed gap down from eight to two, and the flawed draft is still in the project.
Mistakes can be caught before a paper is published, and each correction is filed next to the mistake it fixed.
This record comes from the audit of the same paper. It lists each original claim with the decision made about it and the reason. Certificates
Some proofs come down to a long but finite list of cases. For those, a program checks every case and saves the result as a certificate, and we test the checker on a deliberately broken input to make sure it fails.
Readers can run the check themselves.
The certificate atlas for the Hadwiger paper checks 1,540 pairs and keeps a record for each one.
Research
We have published four papers so far, and all of them are free to read on Zenodo.
Every line that crosses the square hits this fence. Its length is √2 + √6/2, the shortest known.
Sharp reach bounds and quantitative localization for opaque sets
We prove two sharp inequalities for barriers that block every line through the unit square, and show what any barrier shorter than √2 + √6/2 must look like.Clique minors and fractional clique covers in graphs with independence number two
For graphs with independence number two, we turn clique-minor bounds into chromatic bounds without accumulating error, and apply them to Hadwiger’s conjecture.Stationary response and singular limits in a linear zonal gyrokinetic model
We derive the stationary response of a linear periodic gyrokinetic model without assuming uniform kinetic relaxation, and show that two of its limits do not commute.Locality and global information in elliptic solvers
A local approximation to an elliptic inverse needs on the order of nᵈ/(w + 1)ᵈ shared coordinates of global information, and a linear construction achieves this.
