A probabilistic program for theorem proving and autoformalization in Lean 4, powered by GPT-4.
Note: if the executing Lean code is failing, it's almost certainly something wrong with your leanprover-community/repl
The following slides provide additional context for pySagredo.