corpus.blog
56,966 blogs · [ { "id": "01a0878a-89d8-73b1-95eb-1733cf098964", "title": "The Three Types of FOND Planning Policies", "url": "http://jamesoswald.dev/posts/fondpolicytypes/", "published_at": "2026-08-27T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733cf676a25", "title": "What is f(x) ≤ g(x) + O(1)? Inequalities With Asymptotics", "url": "http://jamesoswald.dev/posts/bigoinequality/", "published_at": "2026-02-20T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733cfefb567", "title": "Lean4 Macros for Implementing Custom Quantifiers", "url": "http://jamesoswald.dev/posts/custom-quantifiers-lean/", "published_at": "2025-11-08T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d09bb971", "title": "Extracting Terms from Big Operators on Sequences in Mathlib", "url": "http://jamesoswald.dev/posts/mathlib_sum_and_union/", "published_at": "2025-08-29T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d12e0038", "title": "Status Page Theater", "url": "http://jamesoswald.dev/posts/status-page-theater/", "published_at": "2025-08-17T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d1decb6b", "title": "A Meditation on Extending Inductive Types in Lean4", "url": "http://jamesoswald.dev/posts/meditation-extending-inductive-types/", "published_at": "2025-04-23T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d2934fdf", "title": "A Simple Typeclass for Logic Formulae in Lean4", "url": "http://jamesoswald.dev/posts/a-type-class-for-logic/", "published_at": "2025-04-23T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d2949807", "title": "Emulating Rust's Result and ? in Jai with Metaprogramming", "url": "http://jamesoswald.dev/posts/jai-result/", "published_at": "2025-02-02T00:00:00+00:00" }, { "id": "01a0878a-89d8-73b1-95eb-1733d2bbd449", "title": "A Transcription of John McCarthy's Czechoslovakia Visit Letter", "url": "http://jamesoswald.dev/posts/john-mccarthy-czech/", "published_at": "2024-12-14T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fab122ed1", "title": "Speeding Up Collatz Iteration With Inline Assembly", "url": "http://jamesoswald.dev/posts/collatz-inline-assembly/", "published_at": "2024-12-12T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fab850991", "title": "A Basic Inductive Type Comparison: Rust, Lean, C, C++", "url": "http://jamesoswald.dev/posts/sumtypes/", "published_at": "2024-08-06T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fac23c575", "title": "Embedding, Jai, and Joy (Jai Part 2)", "url": "http://jamesoswald.dev/posts/jai-2/", "published_at": "2024-06-24T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fac7d7ea4", "title": "Simplicity, Jai, and Joy (Jai Part 1)", "url": "http://jamesoswald.dev/posts/jai-1/", "published_at": "2024-06-23T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5facc93b7c", "title": "Inference Rules in Peirce's Alpha Existential Graphs (Part 2)", "url": "http://jamesoswald.dev/posts/alpha-existential-graphs-5/", "published_at": "2024-06-11T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5facf52fc1", "title": "Formalizing The Singularizing Properties Problem", "url": "http://jamesoswald.dev/posts/singularizing-properties-lean/", "published_at": "2024-04-11T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fada43eb3", "title": "The Law of Excluded Middle Does Not Imply the Axiom of Choice", "url": "http://jamesoswald.dev/posts/lem_aoc/", "published_at": "2024-03-29T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fae7ef8a4", "title": "Golfing Rozek's Lean4 Tutorial", "url": "http://jamesoswald.dev/posts/rozeks-lean4-tutorial-golfed/", "published_at": "2024-03-18T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5faf0c9b87", "title": "Proving the Correctness of Insertion Sort in Lean4", "url": "http://jamesoswald.dev/posts/lean4-insertion-sort/", "published_at": "2024-02-18T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fafcf6565", "title": "Worldbuilding Formal and Aesthetic Magic Systems", "url": "http://jamesoswald.dev/posts/logicistmagesmanifesto/", "published_at": "2024-01-04T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fafeb2c93", "title": "Anticode: A Good Minimalist Code Of Conduct", "url": "http://jamesoswald.dev/posts/anticode/", "published_at": "2023-11-03T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fb0e2796f", "title": "Inference Rules in Peirce's Alpha Existential Graphs (Part 1)", "url": "http://jamesoswald.dev/posts/alpha-existential-graphs-4/", "published_at": "2023-10-30T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fb0f90a7e", "title": "A First Look at a Formal Notion for AEG Subgraphs", "url": "http://jamesoswald.dev/posts/alpha-existential-graphs-3/", "published_at": "2023-10-03T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fb1887c05", "title": "Basic Properties of Peirce's Alpha Existential Graphs", "url": "http://jamesoswald.dev/posts/alpha-existential-graphs-2/", "published_at": "2023-08-20T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fb2530ad2", "title": "Propositional Logic in Peirce's Alpha Existential Graphs", "url": "http://jamesoswald.dev/posts/alpha-existential-graphs-1/", "published_at": "2023-07-31T00:00:00+00:00" }, { "id": "01a0878a-89d9-716f-86eb-4e5fb264ba8a", "title": null, "url": "http://jamesoswald.dev/about/", "published_at": null }, { "id": "01a0878a-89d9-716f-86eb-4e5fb2a57fad", "title": null, "url": "http://jamesoswald.dev/contact/", "published_at": null }, { "id": "01a0878a-89d9-716f-86eb-4e5fb2b64330", "title": null, "url": "http://jamesoswald.dev/profiles/", "published_at": null }, { "id": "01a0878a-89d9-716f-86eb-4e5fb2f94e17", "title": null, "url": "http://jamesoswald.dev/publications/", "published_at": null } ] posts Claim your blog
Back to jamesoswald.dev
Blog · corpus.blog/blogs/jamesoswald.dev/posts

jamesoswald.dev

jamesoswald.dev

2026

The Three Types of FOND Planning Policiesoriginal ↗
27 Aug 2026
What is f(x) ≤ g(x) + O(1)? Inequalities With Asymptoticsoriginal ↗
20 Feb 2026

2025

Lean4 Macros for Implementing Custom Quantifiersoriginal ↗
8 Nov 2025
Extracting Terms from Big Operators on Sequences in Mathliboriginal ↗
29 Aug 2025
Status Page Theateroriginal ↗
17 Aug 2025
A Meditation on Extending Inductive Types in Lean4original ↗
23 Apr 2025
A Simple Typeclass for Logic Formulae in Lean4original ↗
23 Apr 2025
Emulating Rust's Result and ? in Jai with Metaprogrammingoriginal ↗
2 Feb 2025

2024

A Transcription of John McCarthy's Czechoslovakia Visit Letteroriginal ↗
14 Dec 2024
Speeding Up Collatz Iteration With Inline Assemblyoriginal ↗
12 Dec 2024
A Basic Inductive Type Comparison: Rust, Lean, C, C++original ↗
6 Aug 2024
Embedding, Jai, and Joy (Jai Part 2)original ↗
24 Jun 2024
Simplicity, Jai, and Joy (Jai Part 1)original ↗
23 Jun 2024
Inference Rules in Peirce's Alpha Existential Graphs (Part 2)original ↗
11 Jun 2024
Formalizing The Singularizing Properties Problemoriginal ↗
11 Apr 2024
The Law of Excluded Middle Does Not Imply the Axiom of Choiceoriginal ↗
29 Mar 2024
Golfing Rozek's Lean4 Tutorialoriginal ↗
18 Mar 2024
Proving the Correctness of Insertion Sort in Lean4original ↗
18 Feb 2024
Worldbuilding Formal and Aesthetic Magic Systemsoriginal ↗
4 Jan 2024

2023

Anticode: A Good Minimalist Code Of Conductoriginal ↗
3 Nov 2023
Inference Rules in Peirce's Alpha Existential Graphs (Part 1)original ↗
30 Oct 2023
A First Look at a Formal Notion for AEG Subgraphsoriginal ↗
3 Oct 2023
Basic Properties of Peirce's Alpha Existential Graphsoriginal ↗
20 Aug 2023
Propositional Logic in Peirce's Alpha Existential Graphsoriginal ↗
31 Jul 2023

Undated

http://jamesoswald.dev/about/original ↗
—
http://jamesoswald.dev/contact/original ↗
—
http://jamesoswald.dev/profiles/original ↗
—
http://jamesoswald.dev/publications/original ↗
—