I would like a thing where I put in a proposition and attempts are made at autocomplete style proofs of the proposition. Maybe you can do that with program synt

I would like a thing where I put in a proposition and attempts are made at autocomplete style proofs of the proposition. Maybe you can do that with program synthesis techniques and Lean style theorem provers.