Alignerr is seeking mathematicians with expertise in Lean 4 to translate informal mathematical proofs into machine-verifiable formal structures. The role involves collaborating with AI researchers to improve formal verification pipelines and identify gaps in automated reasoning tools. Candidates should hold at least a Master's degree in a relevant field and have hands-on experience with formal proof systems.