No, almost none (except for in certain fields, such as HoTT) have formalized proofs.
Why not? It seems like this should sort of be the standard now? Or is it hard to make lean proofs in all fields?
alt Hacker News
Why not? It seems like this should sort of be the standard now? Or is it hard to make lean proofs in all fields?