What kind of harness does the exploration? Where did the corpus of Lean proofs come from? Is the code backing Ton 618 open source?