>And tools like Lean4 aren't limited to constructive math afaik. In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use c

>And tools like Lean4 aren't limited to constructive math afaik. In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.