Lean Engineer

Раз уж новые модели OpenAI умеют решать по 400 задач разом, кому-то стоит воспользоваться этим на благо сейфти. Помните Resolution — большую теоретическую алайнмент-лабу со ставкой на автоматизацию ресёрча? Штош, ресёрч автоматизируется: за неделю их агенты формализовали в Lean доказательство теоремы Хиронаки о разрешении особенностей. Сам Хиронака получил за него Филдса в 1964 году, но доказательство было на двести страниц и такое сложное, что его почти никто не понял. Зачем формализовали? Во-первых, это красивый proof-of-concept того, на что способны агенты — на то, чтобы проделать это руками, ушли бы годы работы нескольких человек. Во-вторых, теорема нужна самим Resolution — она имеет прямое отношение к генерализации моделей, которой они занимаются. И хотя в Хиронаке никто особенно и не сомневался, библиотека с формализацией поможет в будущем ресёрче. Формализация в Lean очень нужна сразу нескольким командам. И поэтому мы ищем Lean Engineer'а. Ни строчки на Lean ему или ей писать не придётся: это будут делать фейблы и астры в таких объёмах, которые человеку охватить не под силу. Задача инженера — организовывать этот процесс надёжным, эффективным и удобным: поддерживать стандарты, помогать ресёрчерам, придумывать, какие нужны общие библиотеки и как сделать так, чтобы аутпутам агентов можно было верить. Требования, в общем-то, логичные: несколько лет опыта с Lean и Mathlib, опыт с автоформализацией и много работы с AI, сильная математика или теоретический CS, вас правда мотивирует алайнмент. Особенно круто, если вы вдруг контрибьютили в Mathlib или работали над формализацией чего-то большого. Перевозят в офис в Беркли, помогают с визой.