“Philosophy, like some people, was prepared to accept boredom in exchange for certainty as it grew to middle age”

seem to have started a job I’m actually really happy with, an incredible feeling

working on an exploratory markov chain notebook for fun, and getting to the point of spending all the time on it getting worse and worse visualizations as I go

having fun trying to finish my project on heyting-valued sets before starting new job

surprising how often I manage to hit this interaction

very aligned with this piece

If M is a C^r manifold then the tangent bundle TM is most naturally a C^r-1 manifold (and more generally the k-jet bundle is most naturally a C^r-k manifold), but in fact any C^r manifold has a unique structure as a C^r+s manifold for any s (including s = ∞)

I wonder if there are versions of finitism that would assent to the theorems that are true in all boolean toposes, and then further wonder if there is a reasonable theory for the "free" boolean topos (essentially HOL + EM) that embodies such principles

before bed I watched the ARIA video of davidad and then I had a dream where he was elected a member of parliament and I was in the chamber to hear his maiden speech

It's out btw dl.acm.org/doi/10.1145/...

Wrote a post on Kripke and Beth semantics in lean 4, and added some features to my blog so that you can see the proof state on hover: boarders.github.io/posts/beth.h...

Lawvere discusses averaging operators or, one might say, ‘voting procedures’. We have a set X and we consider each X making a choice from set V, so the object V^X, a voting procedure is then a function: v : V^X -> V

john mccarthy once remarked that the "it's so over, we're so back" machine had beliefs, to which john searle scoffed "and what beliefs are those john?" to which mccarthy replied "to wit, it has two beliefs: 'it's so over' and 'we're so back'"

every generation thinks they invented it but john rawls was already minmaxxing in the 1950s

have been working on using Verso to get lean developments to render on my blog with hover over proof state - feel happy with the result and will probably write up something about kripke semantics as a reasonable test run

working on basic kripke semanics

moratorium needed on four word sentences with a comma in the middle, no more “same X, different Y”

Wrote a blog post developing the basics of the theory of well-founded relations in agda discussing some of the details of how the theory is handled in a constructive setting:

Wrote a blog post developing the basics of the theory of well-founded relations in agda discussing some of the details of how the theory is handled in a constructive setting:

decided to revive my blog and wrote up my project I did over christmas developing the semantics for simply-typed lambda calculus in a CCC using agda-categories:

tech companies simply love doing five rounds of interviews and then saying nothing more than that they won’t be moving forward

plenty of contemporary people also believe adamantly in homo-pessimism/npc-ist social theory and just substitute the adherents to their brand of political theory as signifying who the great men of history - those that transcend such conditions - are

We're hiring for Bombadil! Come work with me on the future of browser testing — specification languages and temporal logic, JS runtimes, bundlers, and WASM frontends in Rust, and lots and lots of property-based testing. This is onsite in London. Apply here: antithesis.com/company/care...

started a project which was meant to be "learning something about EE" and has gone way off track

Reminder that there is virtually no reason to have an Audible subscription over Libro (which will support your local bookstore)

thought this was rather worthwhile and offers a far more humanistic vision of the future of software engineering (which, of course, traces back to Bret Victor):

Hey I have soundness and completeness of unification in Lean! I'm not sure it's been done (though I wouldn't be shocked). It was harder than I expected, tbh. I should have followed the paper proof more closely. github.com/codyroux/tra...

Really cool haskell project for doing symbolic regression across data: github.com/DataHaskell/...

thinking for the first time in a long while about combinators for term traversals like this one - map over syntax with debruijn indices where we keep some state that is updated as we go under a binder

" The Sphere Spectrum is complicated because it's *free* "

I've written a couple of papers on how Core(FinSet) being the coproduct of all the symmetric groups helps us understand representations of symmetric groups, and how those are related to symmetric functions. Unfortunately the first has an unnecessarily scary title. arxiv.org/abs/2106.00190

proof of eckman--hilton, really leaves something to be desired and I wonder how a nicer version would look (in terms of syntax)

Set doesn’t have a classifier for finite subsets, but if you try to imagine a theory of (2,1) toposes then Grpd has Core(Set) classifying discrete fibrations / families as well as Core(FinSet) classifying finite discrete families

getting started on basic topos theory, will need to take a detour into lattice theory + developing that Hom 1 Ω is a lattice (not sure how to develop that it is an internal lattice object atm)

im starting to worry about this black box of pattern matching on the data it was trained on

This careers page for “Math, Inc.” www.math.inc/careers is just wildly off putting

returning to my learning project of working through 'From Mathematics to Generic Programming' in rust. In chapter 1, stepanov computes an optimized algorithm for "egyptian multiplication" so I tried out kani to verify it (hoping to figure out something it will be genuinely useful for)

if higher order logic is just “set theory in sheep’s clothing” then first-order logic is just finite, complete, atomic Boolean algebra in sheep’s clothing and so would also “not be a logic”

There's a new Francis Spufford. This is not a drill. I repeat, there's a new Francis Spufford.

almost got to some elementary topos theory, can now express that a cartesian closed cat with zero object is degenerate (every hom set is subsingleton)

I thought I'd set up various specialized notions of limits (products, equalizers, pullbacks etc.) and then a theory of general limits as universal cones, and then show the former are special cases of the latter, but in practice it seems surprisingly painful to write out all the details

🙃🙃🙃

The simplest known single axiom for groups in terms of multiplication & inverses: ((z * (x * y)^{-1})^{-1} * (z * y^{-1})) * (y^{-1} * y)^{-1} = x (Source: K. Kunen. Single axioms for groups. J. Automated Reasoning 9 (1992), 291-308)

lots of true mathematics sounds like total crank stuff: understanding only the signature of critical points of a generic smooth function on a manifold allows one to recover its homotopy type, this also works for infinite dim manifolds, and so we can study loop spaces via their energy functional

really starting to wonder if there are limits to the negotiation strategy of “we get everything, you get nothing”

“If formal verification becomes vastly cheaper, then we can afford to verify much more software. […] AI also creates a need to formally verify more software: rather than having humans review AI-generated code, I’d much rather have the AI prove to me that the code it has generated is correct.”

working on the general theory of limits, only got far enough to prove uniqueness before I had to stop

working on basic theory of finite limits, here I am, rather laboriously, proving that having products + equalizers means a cat has pullbacks

moving towards elementary toposes, just got function objects set up to a usable extent and here is eta for exponentials