About

I’m an engineer and researcher interested in a variety of subjects related to math, computer science, economics, etc.

Intent

My intent is for this blog to be a compendium of:

Writings about books, papers or small side projects that I undertake for the purpose of learning, in the hope that my distillations will be useful to others (generally marked “Exposition”).
Widgets that I build in the course of those investigations (code will generally be shared, but use it at your own risk).
Writing about any insights or ideas that I may have related to my interests (generally marked “Research” or “Speculation”).

Subject Areas

I’ll try to keep everything roughly organized by subject, ideally in some sort of pedagogical ordering.

ML Engineering
- Vector Search
  - Basic Vector Search Infra
Reasoning
- E-Graphs
  - E-Graph Basics
- Proof Assistant
Essays
- The Paradox of Taste

Disclaimer

All code and information on this blog is subject to error. Use at your own risk.

Errors

Please let me know if you see any errors.

Recent Posts

Tactics Elaboration

The “reverse-chaining” style proofs (working backward from some desired theorem using out tactics engine) ought to be convertible to “forward-chaining” style proofs (working…

Retrospective: Proof Assistant

I set out to build a proof assistant for a few reasons:

Match Construct

In the Induction post, we were able to build some simple inductive types and write some (very simple proofs). However, the actual process of defining the inductive types and…

Setting up Vector Search in AWS with Pinecone and SST

Frequently, we want the ability to efficiently search and retrieve relevant information based on meaning rather than just keywords. This is a common pattern in LLM-based…

Tactics Engine

Commonly used proof assistants like Coq and Lean don’t prove theorems directly using the typing rules. Rather, they use tactics to reason backwards from some goal to the…

The Paradox of Taste: Borges, Preference Oracles, and the Platonic Theory of Art

In Collected Ficciones (1944), Borges tells the story of the fictional author Pierre Menard. The story is presented in the form of a literary criticism of Menard’s complete…

Sort Hierarchy

In the post on the calculus of constructions, we implemented several Sorts (SProp, Prop, Set, Type). A Sort can be thought of as a “type of types.” For example, booleans and…

Induction

To introduce more complex notions into our type system, we need induction.

Typing Rules

How can we tell if a term is well-typed? How can we tell if an environment is well-formed? We can be sure we have formed a proper term and environment (in the Calculus of…

Conversion Rules

Now that we can represent some basic theorems using a computer, we need to be able manipulate those representations. We also will want to be able to tell if two types are…

Calculus of Constructions

To verify (or prove) theorems using a computer, we need some way to represent a theorem and the steps used to prove it. The Calculus of Constructions (CoC) forms the basis…

E-Graph Basics

An e-graph (equivalence graph) is a type of data structure commonly used to reason about equalities and programs computationally.