A 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...