FORMAL

In FORMAL, we will implement both machine learning algorithms and formal proofs of their performances in the same programming and proof language, Lean. This will enable the use of AI to design new algorithms and derive proofs of their properties. Having access to both implementation and the theoretical proofs that motivated its design at the same time will allow AI agents to get feedback on both in order to improve machine learning algorithms.