The company is looking for expert mathematicians with a Master's degree or higher to translate informal mathematical proofs into machine-verifiable Lean 4 formalizations. The task involves analyzing proofs across various domains to identify gaps and improve formal verification pipelines for AI research. Candidates should have hands-on experience with formal proof systems like Lean, Coq, or Isabelle/HOL.