Blog

We've just received a significant grant for inference from Anthropic, as part of their recent announcement of support for foundations and research institutions.

Kim Morrison and Remy Degenne did an audit of a few formalization quality indicators across several Lean libraries. Our purpose was to see if we could quantify the common assumption that Mathlib is a high-quality library, while AI-generated formalizations perhaps less so, and to see if efforts to improve the quality of AI-generated formalizations could be measured.