Description: this page is dedicated to AI for mathematics and formalization of mathematics, with focus on LEAN.
Formalization of the Lagrange theorem: https://github.com/Moksit/Lagrange-Formalization-Lean
PS: the proof exists already on Mathlib, this repo is dedicated for educational purposes.
Current works: co-authoring research papers on the formalization of mathematics in Lean using LLMs.