alt Hacker NewsA harness [1] was developed by Terrence Tao and some collaborators to prove mathematical results. It has since then been used by others with positive effect. Can someone critique the structure of this harness? I don't know anything about this stuff.
[1] https://github.com/1stproof/batch-2/tree/main/batch-2-submis...
it's not actually proving it though? It's more like stringing it together. A person or LEAN has to actually provde something. I've yet to see anything other than AI-slop produces simulcra of proofs. If it were proving something it'd be <insert mathematician> validates AI proof.