7 ms·
Interesting that this only specialized for Lean4 and not for similar like Coq
by impodimium 3mo ago
Interesting that this only specialized for Lean4 and not for similar like Coq
- DoctorOetker 3mo agoI would have preferred actual proof objects, as in Metamath's: separate the actual proof from the heuristics used to find it (also valuable, but a different thing).