+I would be interested in having volunteers "playtest" the companion (using downstream forks of the repository) to see if this can actually be done (and if the helper lemmas or "API" provided in the Lean files are sufficient to fill in the sorries in a conceptually straightforward manner without having to rely on more esoteric Lean programming techniques). Any other feedback will of course also be welcome. However, I do not intend to place solutions in this repository directly.
0 commit comments