Author: Jiachen Shen, Xiuyuan Lu
This repository contains mathematics proofs from Jeremy Avigad's Mathematics in Lean, originally written in Lean, reworked in Litex.
Litex is formal language that is still under active development. Its design emphasizes simplicity and learnability and is very close to natural language. We hope this repository helps readers get to know Litex and compare it with other formal languages.
Feedback and corrections are welcome on GitHub or at [email protected]. Visit Litex website for more information.
Reference: