Testing Large Language Models’ Autoformalization Capabilities in LEAN

A UW Math AI Lab project. Our goal is to measure and compare Large Language Models' ability to generate formalized LEAN 4 code.