Hacker News Reader

Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.

I've confirmed with the mathematicians working in that field that this is a new result.

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 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.

Reply on news.ycombinator.com