logoalt Hacker News

immmmmm • yesterday at 4:07 PM • 1 reply • view on HN

Aren’t some type systems (eg Lean) able to essentially verify/prove arbitrary mathematics?

Replies

kachnuv_ocasek • yesterday at 5:14 PM

Yes, until you introduce inconsistent axioms. Then you can prove anything.