Formal Verification Research Specialist (Grant Funded)

This NSF-funded, full-time research position will support a project at the intersection of mathematics, computer science, formal verification, and artificial intelligence. The project is working toward a complete and reproducible formal certification in Lean of a fundamental result in harmonic analysis concerning the HRT conjecture. The Research Associate will translate mathematical arguments into formally verified Lean 4 proofs, develop and improve proof code, maintain reproducible project documentation, and support the careful use and evaluation of large language models and automated theorem-proving systems. A central responsibility will be to serve as a human-in-the-loop bridge among mathematicians, large language models, specialized theorem-proving systems, and the Lean compiler and kernel.

This is a grant funded position through December 18, 2026.