← Back to context Comment by impodimium 6 days ago Interesting that this only specialized for Lean4 and not for similar like Coq 1 comment impodimium Reply DoctorOetker 6 days ago I 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).
DoctorOetker 6 days ago I 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).
I 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).