Stories by ngrislain

Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types

Reading Note: Sequential-Parallel Duality in Prefix Scannable Models

Show HN: Lean-pq a typesafe PostgreSQL connector for lean

Don't Vibe – Prove

Lean-PQ – Type-safe PostgreSQL bindings for Lean 4 via libpq FFI

How to Die Optimally – A Theory of Consumption When AI Takes Your Job

Lean Advent of Code 2025

Teaching 3D Geometry with Pyxel

Mathematical Beauty, Truth and Proof in the Age of AI

Post-Labor Economics Lecture 01 [video]

A Practical Method for Testing Differential Privacy – By Andi Cuko

Show HN: Value likelihoods for OpenAI structured output

RAG with Differential Privacy

DP-RAG

Show HN: A simple implementation of Differentially Private RAG

Nostr – Wikipédia

Enhancing May App Service Quality While Safeguarding Patients' Data

Qrlew SQL Framework

Lake Nyos Disaster