Lean4 - How the theorem prover works and why it's the new competitive edge in AI
Large language models struggle with reliability and hallucinations. This article explores how Lean4, an interactive theorem prover, acts as a truth kernel to mathematically verify AI outputs, creating a new standard for deterministic and safe AI.
Nov 23, 2025
Stanford CS336 - Language Modeling from Scratch
Learning internals of LLMs and its components!
Jun 6, 2025