@ertchin@mstdn.social to that matter, if i had $22,000,000 in compute and a copy of Lean, could I have proven a significant number of theorems using random search