Falling in an odd rabbit-hole of visualizing logical deductions.

Why isn't there a mobile friendly game for proving the ~100 core theorems of propositional and first-order logic?

[1] incredible.pm
[2] www.winterdrache.de/freeware/dom...
[3] www.jfsowa.com/peirce/ms514...

AI boosts productivity until a breaking point where domain expertise becomes unnecessary (coding, formalizing math, etc.) - you can go straight from idea to implementation without interaction with the underlying tool. Some are betting that arrives soon enough that they don’t invest in learning.

You can’t convince me Russell wouldn’t have used Lean if he had a chance.

new blog post - Why formalize mathematics - more than catching errors rkirov.github.io/posts/why_le...

Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean.

(An experiment in rigorous math education outside traditional academia)

Newest installment in my journey of learning how to do math proofs with computers rkirov.github.io/posts/lean4/.

The more I learn about logic, it dawns on me that math is sloppy about syntax (“by abuse of notation”), while software engineering is sloppy about semantics (“the purpose of a system is what it does”) and only when analyzing logical systems their interplay is explored.

Ironic that in logic "model" is the thing imbued with meaning (contrasting the syntactic meaningless moving of symbols around), while in ML "model" is the meaningless (but useful) pile of bits, while the "real world" which the ML model models is where the meaning is.

We're excited to share the Lean FRO Year 3 Roadmap today! It builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026.

➡️ Read the roadmap at lean-lang.org/fro/

#LeanProver #FormalMathematics #FormalVerification

New blog post on my learning formal mathematics with Lean journey - rkirov.github.io/posts/lean3/

More notes on learning math theorem proving with Lean - rkirov.github.io/posts/lean2/.

New blog post - learning how to use a dependently typed language Lean4 to write formally verified math proof rkirov.github.io/posts/lean1/

Reflections on using Cursor for a simple, but non-trivial coding task - analysis the board game Ticket to Ride: First Journey
rkirov.github.io/posts/ticket/

If you are looking for puzzle game recommendations, read about the ones that I played and enjoyed in 2024 - rkirov.github.io/posts/puzzle...

New blog post - Advent of Code '24 Retro rkirov.github.io/posts/aoc2024/.