3 ms·
No it's a terrible example. We have ITPs and ATPs and any progress on ATPs, which are the ones that are currently considered magical, are turning into a fine as
by hggigg 2y ago
No it's a terrible example. We have ITPs and ATPs and any progress on ATPs, which are the ones that are currently considered magical, are turning into a fine asymptote. ITPs are useful however but have nothing to do with ML at all.
Putting a confident timescale on this stuff is like putting a timescale on UFT 50 years ago. A lie.
Oh and lets not forget that we need to start with a conjecture first and we can't get any machine to come up with anything even remotely new there.
There is no existential despair. At all.
- auggierose 2y agoI said 30 years, because that's for how long I am a participant in the field. I have a PhD in ITP, and yes, I am pretty confident that automation is a big part of ITP now. Maybe not so much if you are into constructive type theory, that field is always a little bit hesitant to use the full power of anything. The only one lying here is you. To yourself. By the way, AI can come up with conjectures just fine. I might not be interested in most of them, but then again, I am not interested in most conjectures humans come up with.