Alignerr is seeking Lean 4 specialists to translate complex mathematical content, proofs, and theorems into precise, machine-checked formalizations to train AI models. Candidates must have strong hands-on experience with Lean 4 and a solid background in mathematics, formal logic, or formal verification. This is a fully remote, flexible hourly freelance contract role.