ngrislain

5 ms·

1.
by ngrislain 8d ago
Thank you, yes, absolutely, and it's also the perfect language for an AI agents. The more refined the type system, the tighter the feedback loop for the agent.
2.
Like Terraform, but in Lean 4(ngrislain.github.io)
7 points by ngrislain 9d ago|2 comments
3.
by ngrislain 14d ago
I have been using https://www.passwordstore.org/ for 10 years and am super happy with it. It does not provide all the convenient integrations of 1Password though.
4.
Language Models Are Anomaly Detectors(ngrislain.github.io)
2 points by ngrislain 15d ago|0 comments
5.
LaSuite.coop(lasuite.coop)
2 points by ngrislain 16d ago|0 comments
6.
Anomaly Detection with LLMs for Cybersecurity(ngrislain.github.io)
2 points by ngrislain 26d ago|0 comments
7.
Investigate every security event with an AI agent, without the frontier bill(datadoghq.com)
2 points by ngrislain 2mo ago|0 comments
8.
Vibe Under Constraint - Claude Code writing Lean 4(ngrislain.github.io)
3 points by ngrislain 3mo ago|1 comments
9.
by ngrislain 3mo ago
Vibe coding is great. You describe what you want, the agent writes it, the tests pass, you ship. It keeps working right up to the moment it does not: the job gets killed by the OOM reaper in production, or it opens ten thousand file descrip
10.
by ngrislain 4mo ago
100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale
11.
Mamba-3 and the State Space Model Renaissance(ngrislain.github.io)
1 points by ngrislain 5mo ago|0 comments
12.
The Signature Method in Machine Learning (an interactive reading note)(ngrislain.github.io)
1 points by ngrislain 5mo ago|0 comments
13.
by ngrislain 6mo ago
Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.
14.
by ngrislain 6mo ago
You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.
15.
by ngrislain 6mo ago
Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.
16.
Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types(ngrislain.github.io)
34 points by ngrislain 6mo ago|23 comments
17.
Reading Note: Sequential-Parallel Duality in Prefix Scannable Models(ngrislain.github.io)
2 points by ngrislain 6mo ago|0 comments
18.
Show HN: Lean-pq a typesafe PostgreSQL connector for lean(github.com)
2 points by ngrislain 6mo ago|1 comments
19.
Don't Vibe – Prove(ngrislain.github.io)
4 points by ngrislain 6mo ago|0 comments
20.
Lean-PQ – Type-safe PostgreSQL bindings for Lean 4 via libpq FFI(github.com)
1 points by ngrislain 7mo ago|0 comments
21.
How to Die Optimally – A Theory of Consumption When AI Takes Your Job(ngrislain.github.io)
2 points by ngrislain 7mo ago|0 comments
22.
by ngrislain 9mo ago
Just finished
23.
by ngrislain 10mo ago
Yes, I'm doing it without AI to learn the language, nonetheless I do think that Lean 4 + AI is a super-powerful combination.
24.
by ngrislain 10mo ago
Yes, this year I'm going for Lean 4: https://github.com/ngrislain/lean-adventofcode-2025 It's a great language. It's dependent-types / theorem-proving-oriented type-system combined with AI assistant
25.
by ngrislain 10mo ago
A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849
26.
Lean Advent of Code 2025(github.com)
1 points by ngrislain 10mo ago|2 comments
27.
by ngrislain 10mo ago
Advent of Code 2025 in Lean...
28.
Teaching 3D Geometry with Pyxel(ngrislain.github.io)
1 points by ngrislain 10mo ago|0 comments
29.
Mathematical Beauty, Truth and Proof in the Age of AI(quantamagazine.org)
2 points by ngrislain 1y ago|0 comments
30.
Post-Labor Economics Lecture 01 [video](youtube.com)
2 points by ngrislain 1y ago|0 comments

More ›