AxIOM

A challenging aspect of computer formalization is formalizing definitions that are (i) mathematically correct (something that is not automatically verifiable and must be checked by human experts), (ii) optimized for usability and (iii) at the appropriate level of generality. The AxIOM "Building the mathematical library of the future" will focus on formalizing definitions in Lean across a wide range of mathematical subject areas in the hope that it will be possible to correctly formalize the statements of recent theorems from the research literature. Such work is essential for making formal verification tools more relevant to mathematics researchers.