corpus.blog
41554 blogs · [ { "id": "01a087d5-583f-719e-aa07-3d5df8d46e21", "title": "The Jacobian Challenge Retro", "url": "https://rkirov.github.io/posts/jacobian/", "published_at": "2026-06-22T22:14:33+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5df928c478", "title": "Virtuous intellectual chores - now optional", "url": "https://rkirov.github.io/posts/virtuous_chores/", "published_at": "2026-05-27T02:11:14+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5df9fa1c2b", "title": "Three Cultures of Math", "url": "https://rkirov.github.io/posts/three-cultures-of-math/", "published_at": "2026-05-09T03:45:53+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfa1c5d65", "title": "From Painfully Explicit to Implicit in Lean", "url": "https://rkirov.github.io/posts/lean-implicits/", "published_at": "2026-04-12T16:25:28+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfa98e56b", "title": "Code Proven to Work - The Math Way", "url": "https://rkirov.github.io/posts/code-proof/", "published_at": "2026-03-23T00:25:24+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfb0ce1c6", "title": "Human Intuition, AI Formalization: A Real Analysis Case Study", "url": "https://rkirov.github.io/posts/lean6/", "published_at": "2026-03-09T06:35:37+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfbaf9e40", "title": "From Sets in Math to Types in Lean: Subtype, Fin, Set, Finset, and Fintype", "url": "https://rkirov.github.io/posts/sets-vs-types/", "published_at": "2026-02-15T04:54:04+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfbe2071d", "title": "Leaning on AI", "url": "https://rkirov.github.io/posts/lean5/", "published_at": "2026-02-09T05:16:11+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfcbe29db", "title": "Local Lean Workgroup Retro", "url": "https://rkirov.github.io/posts/lean_workgroup/", "published_at": "2026-02-01T22:04:19+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfd8cc2e1", "title": "Is this JS function pure?", "url": "https://rkirov.github.io/posts/pure/", "published_at": "2025-11-12T04:18:26+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfe2edc04", "title": "Why formalize mathematics - more than catching errors", "url": "https://rkirov.github.io/posts/why_lean/", "published_at": "2025-10-17T05:32:49+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dfeaa8487", "title": "Learning Lean: Part 4", "url": "https://rkirov.github.io/posts/lean4/", "published_at": "2025-09-20T14:54:08+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5dff6cdd16", "title": "Learning Lean: Part 3", "url": "https://rkirov.github.io/posts/lean3/", "published_at": "2025-06-28T05:30:30+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e00328f8d", "title": "Thoughts on Signals in the JavaScript Ecosystem", "url": "https://rkirov.github.io/posts/signals/", "published_at": "2025-03-30T15:05:09+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e00d4b461", "title": "Learning Lean: Part 2", "url": "https://rkirov.github.io/posts/lean2/", "published_at": "2025-03-02T15:14:48+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e012919d2", "title": "Learning Lean: Part 1", "url": "https://rkirov.github.io/posts/lean1/", "published_at": "2025-02-12T06:26:55+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e01ab6c4e", "title": "Ticket to Ride: First Journey simulation authored with AI", "url": "https://rkirov.github.io/posts/ticket/", "published_at": "2025-01-18T19:52:17+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e0217f17f", "title": "Puzzle games of 2024", "url": "https://rkirov.github.io/posts/puzzles2024/", "published_at": "2024-12-31T19:42:13+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e02ff047e", "title": "Advent of Code 2024 Retro", "url": "https://rkirov.github.io/posts/aoc2024/", "published_at": "2024-12-26T05:40:07+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e032b88f4", "title": "Incremental Computation (part 3)", "url": "https://rkirov.github.io/posts/incremental_computation_3/", "published_at": "2020-05-19T00:00:00+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e032d3adb", "title": "Incremental Computation (part 2)", "url": "https://rkirov.github.io/posts/incremental_computation_2/", "published_at": "2020-05-10T00:00:00+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e033d8f43", "title": "Incremental Computation (part 1)", "url": "https://rkirov.github.io/posts/incremental_computation/", "published_at": "2020-05-03T00:00:00+00:00" }, { "id": "01a087d5-583f-719e-aa07-3d5e037a7c5f", "title": "About", "url": "https://rkirov.github.io/about/", "published_at": "2020-04-27T06:05:21+00:00" } ] posts Claim your blog
Back to rkirov.github.io
Blog · corpus.blog/blogs/rkirov.github.io/posts

rkirov.github.io

rkirov.github.io

2026

The Jacobian Challenge Retrooriginal ↗
22 Jun 2026
Virtuous intellectual chores - now optionaloriginal ↗
27 May 2026
Three Cultures of Mathoriginal ↗
9 May 2026
From Painfully Explicit to Implicit in Leanoriginal ↗
12 Apr 2026
Code Proven to Work - The Math Wayoriginal ↗
23 Mar 2026
Human Intuition, AI Formalization: A Real Analysis Case Studyoriginal ↗
9 Mar 2026
From Sets in Math to Types in Lean: Subtype, Fin, Set, Finset, and Fintypeoriginal ↗
15 Feb 2026
Leaning on AIoriginal ↗
9 Feb 2026
Local Lean Workgroup Retrooriginal ↗
1 Feb 2026

2025

Is this JS function pure?original ↗
12 Nov 2025
Why formalize mathematics - more than catching errorsoriginal ↗
17 Oct 2025
Learning Lean: Part 4original ↗
20 Sept 2025
Learning Lean: Part 3original ↗
28 Jun 2025
Thoughts on Signals in the JavaScript Ecosystemoriginal ↗
30 Mar 2025
Learning Lean: Part 2original ↗
2 Mar 2025
Learning Lean: Part 1original ↗
12 Feb 2025
Ticket to Ride: First Journey simulation authored with AIoriginal ↗
18 Jan 2025

2024

Puzzle games of 2024original ↗
31 Dec 2024
Advent of Code 2024 Retrooriginal ↗
26 Dec 2024

2020

Incremental Computation (part 3)original ↗
19 May 2020
Incremental Computation (part 2)original ↗
10 May 2020
Incremental Computation (part 1)original ↗
3 May 2020
Aboutoriginal ↗
27 Apr 2020