tl;dr: Lean Engineer, Berkeley, $346k–930k/year

Раз уж новые модели OpenAI умеют решать по 400 задач разом, кому-то стоит воспользоваться этим на благо сейфти. Помните Resolution — большую теоретическую алайнмент-лабу со ставкой на автоматизацию ресёрча?

Штош, ресёрч автоматизируется: за неделю их агенты формализовали в Lean доказательство теоремы Хиронаки о разрешении особенностей. Сам Хиронака получил за него Филдса в 1964 году, но доказательство было на двести страниц и такое сложное, что его почти никто не понял.

Зачем формализовали? Во-первых, это красивый proof-of-concept того, на что способны агенты — на то, чтобы проделать это руками, ушли бы годы работы нескольких человек. Во-вторых, теорема нужна самим Resolution — она имеет прямое отношение к генерализации моделей, которой они занимаются. И хотя в Хиронаке никто особенно и не сомневался, библиотека с формализацией поможет в будущем ресёрче.

Формализация в Lean очень нужна сразу нескольким командам. И поэтому мы ищем Lean Engineer'а. Ни строчки на Lean ему или ей писать не придётся: это будут делать фейблы и астры в таких объёмах, которые человеку охватить не под силу. Задача инженера — организовывать этот процесс надёжным, эффективным и удобным: поддерживать стандарты, помогать ресёрчерам, придумывать, какие нужны общие библиотеки и как сделать так, чтобы аутпутам агентов можно было верить⚡️

Требования, в общем-то, логичные:
⭐️несколько лет опыта с Lean и Mathlib
⭐️опыт с автоформализацией и много работы с AI
⭐️cильная математика или теоретический CS
⭐️вас правда мотивирует алайнмент

🐱 Особенно круто, если вы вдруг контрибьютили в Mathlib или работали над формализацией чего-то большого.

Перевозят в офис в Беркли, помогают с визой. Платят роскошные $346k–930k в год

Пишите @a_nro🤍