Sieve

Inspiration

I've been following formal mathematics and auto-formalization for about a year now. These two technologies have entirely transformed how mathematics is done. We now have an abundance of proofs but digesting these proofs is more difficult than ever. LLMs are pretty bad at helping us understand these proofs since they struggle with finding "interesting" parts of a proof and with mathematical communication.

What it does

Sieve is a tool for making formal proofs easier to understand. It extracts a proof’s theorems and definitions, then traces the dependencies behind each result. Sieve uses these relationships to construct a graph and identify the theorems and definitions that may be the most "interesting." "Interesting" is hard to define but there's a lot of metrics we can use, which we'll get into below.

How I built it and challenges I ran into

I first started out by trying to figure out how I could extract all the data that Lean proofs hold. Once I had that data, my next big challenge was trying to analyze that data to produce useful insights. Figuring out if a theorem is "interesting" is really difficult. Instead of tackling that problem directly I opted to try and define metrics that could indicate if a theorem was interesting. An example of such a metric is how "connected" a theorem is. For a theorem to be highly connected it must form a bridge between two areas of math that don't share much in common (they don't have many existing bridges between them).

What's next for Sieve

There's a lot more that can be done with the rich data that Lean provides. We can try to define more metrics and find more patterns that may indicate a theorem's usefulness. Sieve also struggles with performance issues when given massive lean proofs. At a certain size Sieve just cannot hold a proof in memory so we need a better solution like indexing into a database.

Built With

• javascript
• lean
• rust