Entry 021 ProgressLasm: running proven Lean code on Node
exit 0Ran itIt works. The server written in Lean answered, and a false theorem failed the build.
- Day 3Active
- Day 7Upcoming
- Day 15Upcoming
- Day 30Upcoming
- Day 90Upcoming
- Day 180Upcoming
- Day 365Upcoming
Latest check Day 3, Mon 2026.11.02
- Commits since launch
- 0 → 76
- Stars
- 79 → 88
- Latest release
- v0.3.6
- Last commit
- 2026.11.01
- HN points
- 34 → 38
Numbers by checkpoint
| Checkpoint | Checked | State | Commits since launch | Stars | Releases | Contributors | Last commit |
|---|---|---|---|---|---|---|---|
| Day 1 | Sat 2026.10.31 | 0 | 79 | 14 v0.3.5 | 2 | 2026.10.28 | |
| Day 3 | Mon 2026.11.02 | Active | 76 | 88 | 15 v0.3.6 | 2 | 2026.11.01 |
| Day 7 | Due Fri 2026.11.06 | Upcoming | |||||
| Day 15 | Due Sat 2026.11.14 | Upcoming | |||||
| Day 30 | Due Sun 2026.11.29 | Upcoming | |||||
| Day 90 | Due Thu 2027.01.28 | Upcoming | |||||
| Day 180 | Due Wed 2027.04.28 | Upcoming | |||||
| Day 365 | Due Sat 2027.10.30 | Upcoming | |||||
What changed
Day 3 Mon 2026.11.02
- An app built with `--target vercel-edge` now deploys to Vercel from a fresh checkout. Before, the deployment omitted the Vercel function file generated by the build (v0.3.6).
- The example app Conduit now runs on Netlify, Fastly, wasmtime and Spin. Its proofs now include a theorem that sign-up stores only the password’s hash and that no reply contains the password.
- Lean no longer hangs when it calls a JavaScript callback synchronously. The maker says 0.3.7 has the fix but was not published. The fix will ship in 0.3.8.