|
|
|
|
|
by nyrikki
1224 days ago
|
|
They are talking about ML, which is statistical pattern matching and finding. Gödel ruined the fun of automated theorem testing a century ago unless we make significant discoveries in math. Type inference is an accessable example of SOTA automated reasoning if you want a more realistic idea of what our current constraints are. We will be restricted to Human assisted Turing machines for the foreseeable future unless there is a major development in pure math. Remember we can't even build a logically consistent model of arithmetic due to Gödel. |
|