(@boarders)

@boarders

Thanks to impermanence all things are possible Working on a book on topos theory

2,283 Following973 Followers3,204 Posts

X YouTube YouTube Bluesky

Is this your profile?Claim it and boarders.dirty.social is yours.Claim profile

boarders@boarders· 20d

working on an implementation of synthetic differential geometry in lean

boarders@boarders· Jul 3

wrote a lean proof of the solution to the MU puzzle from gödel, escher, bach

definition of MIU proof system in lean from Gödel, Escher, Bach

proof of the mod 3 invariant that holds of the MIU proof system

boarders@boarders· Jul 1

from the opening to pete wolfendale’s new book The Revenge of Reason

Screenshot of text reading: “If you think that you can't be studied as an information processing system, and that this allows you to wall off your intuitive conceptions of not just the human condition but what is good in this condition, then I'm afraid there's an oncoming wave that will crest those walls and drown your parochial ambitions. The promise made by neorationalism isn't that this wave is empirical science come to show you the horrors or your neuronal substrate, but that it is mathematical science come to show you the wonders of your computational soul.
We are non-terminating processes interacting with our environment and with one another, exploring the mathematical and empirical realms together, playing games of proof and refu-tation, and building systems and models that are beginning to encompass our own selves.
We are beautiful. We are free. Computational self-consciousness will only enhance this, even if it changes our understanding of what it means.”

boarders@boarders· Jun 28

Added tested --examples which is also searchable, this one showing how comparing fits together with the alternative operator <|> the language has

output showing jq-style tool called birdq with searchable --examples

boarders@boarders· Jun 25

have been working on my own haskell-ish json query language (which also compiles to jq) and I'm really starting to be happy with how it looks

terminal showing various queries to a binary called birdq in the style of a haskell-ish version of jq showing coloured terminal output

boarders@boarders· Jun 19

incredible final sentence recommendation

Photo of text of an opening of a chapter titled “Homotopy” of a book with the following text:
“Suppose that you are standing on a geometrical object (say on the Pampas). You toss a lasso and try to shrink it to a single point at your feet (the lasso must stay on dry ground). If there is no pool of water on this grassland the lasso will smoothly converge at your feet. Imagine, however, that there is a pool of water which your lasso is enclosing (We assume that the interior of the pool does not belong to our geometrical object). In this case you cannot bring the lasso to a single point without getting it wet. The fundamental group or the first homotopy group of the Pampas measures the degree of the possibility in shrinking the lasso to a point.

On the other hand the second homotopy group of a geometrical object measures the degree to which one can shrink a large piece of cloth, spread out with its border being gathered at a single point, to that point while keeping the cloth always in the object.

If the above explanation gives you some idea of what is going on, you might skip this chapter and proceed to the next one.”

boarders@boarders· Apr 29

if you'll believe it my current rough notes have this exact sentence since the first model I consider is exactly just a wrapper around Callable[[V], V] (sadly writing python as this is what is available in colab)

boarders@boarders· Apr 28

[continuing] illustration of the central limit theorem for a random walk. You flip a coin and if it is tails you stay where you are, if it is heads you flip another coin and go left on tails and right on heads. After 1000 steps where you end up closely mirrors a gaussian (with variance √(250 · 1/2))

boarders@boarders· Apr 27

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

extremely messy image of discrete markov chain

boarders@boarders· Apr 24

Image of the quote: “One can argue over the merits of most books... one does not argue about The Wind in the Willows. The young man gives it to the girl with whom he is in love, and if she does not like it, he asks her to return his letters. The old man tries it on his nephew, and alters his will accordingly. ... When you sit down to [read] it, don't be so ridiculous as to suppose you are sitting in judgment on my taste, or on the art of Kenneth Grahame. You are merely sitting in judgment on yourself. You may be worthy; I don't know. But it is you who are on trial."

boarders@boarders· Apr 24

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

lean code showing calc block to prove something basic about Scott's version of presheaves

boarders@boarders· Apr 23

surprising how often I manage to hit this interaction

boarders@boarders· Mar 26

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

example screenshot of proof with hover proof state

boarders@boarders· Mar 25

working on basic kripke semanics

proof of monotonicity for kripke semantics in lean 4

boarders@boarders· Mar 19

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

unicode box diagram with a NAND circuit to compute XOR

boarders@boarders· Mar 16

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

ocaml code for mapping over lambda calculus syntax with debruijn indices

boarders@boarders· Mar 6

in comparison this agda proof is too wordy but syntactically v pleasing

boarders@boarders· Mar 6

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

boarders@boarders· Mar 4

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)

boarders@boarders· Mar 3

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)

rust code worker function which is the main loop for optimized egyptian multiplication

rust code for version of optimized egyptian multiplication that stepanov gives

kani property that this agrees with builtin multiplication or u32 in a given (small) range

terminal showing kani out put for successful verification

boarders@boarders· Mar 2

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)

lean 4 proof that a CCC with zero object is degenerate

boarders@boarders· Feb 27

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

lean 4 proof that having universal cones for product diagrams implies a category has products in the elementary sense

boarders@boarders· Feb 27

🙃🙃🙃

$lean 4 error message saying: Tactic `rewrite` failed: Did not find an occurrence of the pattern mediate' ≫ universal_cone.C₀ { el := 0 } in the target expression T_cone.C₀ { el := 0 } = mediate' ≫ universal_cone.C₀ { el := 0 }$

boarders@boarders· Feb 26

excerpt from Simon Prince's book Understanding Deep Learning which reads:
"The title is also partly a joke — no-one really understands deep learning at the time of writing. Modern deep networks learn piecewise linear functions with more regions than there are atoms in the universe and can be trained with fewer data examples than model parameters. It is neither obvious that we should be able to fit these functions reliably nor that they should generalize well to new data."

boarders@boarders· Feb 26

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

boarders@boarders· Feb 25

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

lean 4 proof that having products + equalizers gives pullbacsks

boarders@boarders· Feb 23

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

lean 4 proof of eta for function objects

boarders@boarders· Feb 21

Proving Type has Prop as a subobject classifier: essentially amounts to some miniature version of the grothendieck construction where you take a mono i : X -> Y to the prop : Y -> Prop, \y -> fiber i y

lean 4 proof that Type u has a subobject classifier, most details off screen and essentially unreadable

boarders@boarders· Feb 18

finally parried but was right to be put off, looks like you need a phd to write this basic proof (only looks so, for I am a drop out)

long lean 4 proof that maps (f : c -> d) induces maps from Sub d to Sub c (sub-objects of an object)

boarders@boarders· Feb 18

into the familiar feeling of getting stunlocked by the goal