jsmorph
Joined 16 years ago
Karma
240
Submissions
20
Member since
Dec 29
Recent submissions
Comment · 4 months ago
Comment · 6 months ago
Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
Comment · 6 months ago
Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html uses a Go/Lean hybrid design. The Go code is mostly glue, and the Lean code is the logic https://github.com/agentcourt/adjudication/tree/main/arb/eng.... It's not math-intensive. Really just functional programming with some interesting proofs (including soundness ideally). Go code can migrate to Lean code when that makes sense.
Comment · 3 years ago
The section [0] on pattern matching [1] was an important inspiration for
some pattern matching that's running in large-scale production today [2].
[0] https://norvig.github.io/paip-lisp/#/chapter5?id=_52-pattern...
[1] https://github.com/norvig/paip-lisp/blob/main/lisp/patmatch....
Comment · 3 years ago
Same. Maybe a GPT-driven super-tactic.
Comment · 4 years ago
Comment · 5 years ago
https://www.inaturalist.org/ also does this kind of thing. iNaturalist works well for lots of different organisms.
Comment · 12 years ago
I hope this group can figure out a master contributor license agreement. Getting together N bilateral CLAs is not ideal.
https://github.com/jsmorph/leanexe
I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ?
https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be...
Fun.