Geoffrey Irving
@geoffreyirving
Cofounder and Chief Scientist at Resolution. Alignment will be solved, but not necessarily in time. Previously AISI, DeepMind, OpenAI, Google Brain, etc.
가입 September 2009
372 팔로잉 중 17.7K 팬
BTW I tried for a while over the last couple weeks to prove a full Lean kernel correct and failed (in the spirit of also mentioning failed attempts). :)
I should make the prediction:
80% that the type theory difficulties in Lean are resolved within a month.
40% that they are resolved within a week.
