From 5df50a2c600038085bb7d55a842b83670e47059d Mon Sep 17 00:00:00 2001 From: Brando Miranda Date: Tue, 24 Sep 2024 19:03:04 -0700 Subject: [PATCH] Update readme.md --- examples/lean4_dsp/readme.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/examples/lean4_dsp/readme.md b/examples/lean4_dsp/readme.md index eefb2db..f605932 100644 --- a/examples/lean4_dsp/readme.md +++ b/examples/lean4_dsp/readme.md @@ -1,4 +1,6 @@ -# +# Lean Draft Sketch Prove (DSP) + +based on Sean Welleck's DSP for Isabelle: https://github.com/wellecks/ntptutorial/tree/main/partII_dsp ## Related work @@ -29,4 +31,4 @@ Questions: - Q1: what is this: "we perform deduplication by problem statements" when does it matter? All MATH train are unique, so why would I care about this? Idea: -- Idea1: use the formal ground truth solution string in MATH, implement Draft Sketch Proof (DSP) for Lean4 + use some symbolic/ntp solver (hammer/tidy/ReProver) \ No newline at end of file +- Idea1: use the formal ground truth solution string in MATH, implement Draft Sketch Proof (DSP) for Lean4 + use some symbolic/ntp solver (hammer/tidy/ReProver)