•••••••••• ищет Lean Engineer для организации процесса формализации математики с помощью AI-агентов.
Обязанности: поддерживать стандарты формализации, помогать исследователям, определять необходимые общие библиотеки и повышать надёжность и удобство проверки результатов агентов.
Требования:
- Несколько лет опыта работы с Lean и Mathlib
- Опыт автоформализации и значительный опыт работы с AI
- Сильная математическая подготовка или знания теоретической информатики
- Искренняя мотивация работать над alignment
Будет плюсом: вклад в Mathlib или опыт работы над крупной формализацией.
Переезд в офис в Беркли и помощь с визой. Зарплата — $346k–930k в год.