20
you are viewing a single comment's thread
view the rest of the comments
view the rest of the comments
this post was submitted on 26 Jul 2026
20 points (100.0% liked)
TechTakes
2627 readers
44 users here now
Big brain tech dude got yet another clueless take over at HackerNews etc? Here's the place to vent. Orange site, VC foolishness, all welcome.
This is not debate club. Unless it’s amusing debate.
For actually-good tech, you want our NotAwfulTech community
founded 3 years ago
MODERATORS
And a follow-up by talia ringer, who observes that there have always been gaps between the type-theoretic underpinnings of things like the lean prover and their actual implementation, and this hasn’t been so much of an issue til now because theorem provers haven’t had the attention of people in high places, and the type-theoreticians have been able to catch up in due course.
https://mathstodon.xyz/@TaliaRinger/117005740997367321
Anyone want to place any bets on whether or nor the big llm companies are going to fund academic research that isn’t obviously mechanisable right now and won’t yield any clickbait headlines?
See also a question asked today on Math Overflow, "Are we stuck with Lean?". The proposed alternative, Metamath, isn't type-theoretic and thus skips the entire dialogue between type theory and proof assistants.