Viewing profile — jsmorph

Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean. https://github.com/jsmorph/leanexe I think I managed to use Talos…

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 (go…

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://gith…

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…

Same. Maybe a GPT-driven super-tactic.

[0] https://en.wikipedia.org/wiki/Homotopy_type_theory [1] https://homotopytypetheory.org/book/

https://www.inaturalist.org/ also does this kind of thing. iNaturalist works well for lots of different organisms.

I hope this group can figure out a master contributor license agreement. Getting together N bilateral CLAs is not ideal.

Here's a colorization based on compositeness: http://blog.morphism.com/2010/05/building-numbers.html

Similar visualizations here: http://blog.morphism.com/2010/05/building-numbers.html http://blog.morphism.com/2010/07/pdfs-from-building-numbers.html That stuff was generated using …