3 ms·

Backtracking idea is interesting, could maybe diffusion help? At some point it turns into sat solving.

• grafmax 1y ago
  Sat solving I guess because types encode proofs?
  • deleted 1y ago
    [deleted]
• deleted 1y ago
  [deleted]