Congratulations

Stream: Berkeley Lean Seminar

[Kevin Buzzard]

Many congratulations to all of you for the insolvability result, and especially for keeping going when the Coq team announced their version. Working on hard problems is the way to make the library better because it reveals problems and gaps in it. Thank you all!