Regardless of whether the target result(s) are ultimately correct, isn't it almost guaranteed that supporting infrastructure for surreals-in-lean is a real contribution? Is it a goal to make those polished/reusable, or more like throw-away harness, and just a stepping stone to the proof?
I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into <a href="https://github.com/vihdzp/combinatorial-games" rel="nofollow">https://github.com/vihdzp/combinatorial-games. Violeta, who maintains CG, expressed interest in ultimately integrating the proof in some shape into the repo, but I think more work needs to be done to understand what makes it work.
j2kun · · focus · HN ↗
danabramov · · focus · HN ↗
ianjbutler · · focus · HN ↗
danabramov · · focus · HN ↗