Formal Verification Research Specialist (Grant Funded)

Formal Verification Research Specialist (Grant Funded)

Title - Formal Verification Research Specialist (Grant Funded)

Position Summary - 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.

Position Type - Temporary

Essential Duties - Develop, test, debug, and maintain formal proofs in Lean 4 and Mathlib. Translate mathematical definitions, lemmas, theorem statements, and proof arguments into precise Lean formulations. Use OpenAI ChatGPT, particularly GPT-5.6 and successor models, to support mathematical analysis, theorem decomposition, Lean code development, proof repair, documentation, and project planning. Use Aristotle and comparable AI-assisted theorem-proving systems to propose, test, repair, and review Lean proofs. Serve as an intermediary among mathematicians, large language models, automated theorem-proving systems, and the Lean compiler. Design effective prompts, task specifications, and iterative proof-development workflows. Review AI-generated mathematical arguments and Lean code for correctness, completeness, theorem-statement fidelity, and compatibility with the project's exact Lean environment. Diagnose Lean elaboration errors, type errors, missing dependencies, indexing problems, and theorem-interface mismatches. Run local builds, regression tests, dependency inspections, axiom checks, machine audits, and reproducibility tests. Ensure that certified proofs do not rely on sorry, admit, unauthorized axioms, unsafe declarations, implemented_by, or other unverified shortcuts. Maintain the project's Git and GitHub repositories, branches, commits, proof files, build scripts, and checkpoint records. Prepare detailed technical documentation, including theorem specifications, proof plans, build instructions, audit reports, reviewer packets, and reproducibility packages. Compare formal Lean statements with the corresponding results in the mathematical literature. Participate in regular project meetings and clearly communicate progress, technical obstacles, mathematical concerns, and proposed solutions.

Required Qualifications - Master's degree in Computer Science or Mathematics. Demonstrated programming ability and experience with typed or functional programming languages. Experience with Lean 4, Mathlib, or a closely comparable interactive theorem prover. Ability to read advanced mathematical arguments and translate them into formal definitions, theorem statements, and proof obligations. Experience using OpenAI ChatGPT or comparable frontier large language models for coding, mathematical reasoning, research, or formal verification. Ability to work with GPT-5.6 and successor OpenAI models in advanced reasoning, coding, tool-use, and compiler-assisted workflows. Ability to use or quickly learn Aristotle and comparable AI-assisted theorem-proving systems. Experience working in Linux or another command-line development environment. Experience with Git, GitHub, branching, commits, merges, and reproducible source-control practices. Ability to diagnose compiler errors and systematically repair formal proof code. Strong analytical, organizational, and problem-solving skills. Excellent written communication and technical documentation skills. Ability to work independently while following strict proof-development, testing, audit, and review procedures. Availability to work 40 hours per week for the duration of the appointment.

Preferred Qualifications - Substantial experience developing nontrivial formal proofs, mathematical libraries, or verified software in Lean 4 and Mathlib. Direct experience using Aristotle or another specialized AI-assisted theorem-proving model or agent to generate, repair, test, or review Lean proofs. Background in formal methods, automated reasoning, programming-language theory, proof engineering, functional programming, or a closely related area. Experience designing and operating agentic or multi-model workflows that integrate large language models, external tools, APIs, version-control systems, compilers, proof assistants, and human review. Demonstrated experience critically auditing AI-generated mathematical arguments, formal proof code, or software for correctness, completeness, reproducibility, and compliance with stated requirements, rather than accepting model-generated output without independent verification.