← Feed

Posts

• View post

  ALL HAIL LORD TRANS

• View post

  This change I'm helping shepherd into Iris-Lean is somehow radicalizing me even more. We're working on changing the algebraic hierarchy to be based on ORA's instead of CMRA's, but because Lean has good typeclasses, we can actually do this swap Indiana Jones style with essentially zero impact on clients who use CMRA. It's kind of like how Iris-Rocq has a MRA construction, but you'll notice.... no MRA canonical structures. I understand that this ki...

• View post

  Today's scripture verse comes from the proof irrelevance chapter

• View post

  Feelin like making a change to View. Prepare for a shitstorm.

• View post

  Extremely satisfying to work in the "putting things into their proper places" factory

• View post

  I have acquired Full body skeleton suit

• View post

  https://github.com/leanprover-community/iris-lean/pull/688 I've posted a few times about it but I think my work here is done. I am now very very pleased with this PR. Fully swapped the theory underlying Iris with essentially zero changes for clients (or at least for the HeapLang client). Might be my favorite piece of code I've ever written, I feel like a proof ninja.

• View post

  I'm gonna do a fun project today

• View post

• View post

  Brutal week to be a Lean Lover

• View post

  A textbook starting off with a definition I dislike. Oh boy.

• View post

  I caved and shelled out an additional $70 to not depart at 5:45 AM tomorrow (now I can leave my house at a luxurious 5:50 instead of a time starting with a 4)

• View post

  In trying a thing where I read a textbook with sticky notes in hand, and I use it to fill in the missing little proofs. It's too early to tell for sure but I really like this! I've noticed it forces me to really understand the definitions eagerly and at a low level (instead of just getting the high level picture and being lost 20 pages later) which is especially useful in probability where the notation is horrible.

• View post

  I'm picturing a "Keep Austin Weird" style campaign to "Make Providence Be Anything"

• View post

  Brown has a lot of similarities to the Tufts Downhill Skatepark in terms of skatability

• View post

  I am in the podunk hamlet of Providence RI

• View post

  I don't think I truly appreciated how far ahead mathlib is compared to the other analysis libraries I have used. Half of the people at this workshop are just... regular mathematicians. And we're talking through theorems I understand maybe 5% of as a "realistic next step". AND this whole workshop is being framed as "Analysis is less supported than algebra in mathlib let's change that". Your "less supported" is my &...

• View post

  I have the wonderful ability to be social xor sober

• View post

  Damn my internship this summer might actually fall apart due to immigration reasons

• View post

  Providence is what I imagine ohio is like from all the rude jokes on Instagram

• View post

  Possibly this is tainted by my negative mood but I think Providence is the worst place on the planet and it should be sunk like a pathetic atlantis

• View post

  Why do they call it main when it's a state full of side characters

• View post

  I have officially closed the Lean Zulip. Not opening it until Thursday unless the shakes get really bad

• View post

  I am hatching a plan to get into the Rivoli as we speak

• View post

  I may be slightly falling in love with Toronto

• View post

  Bird I have an idea

• View post

  lol https://red-squares.cian.lol

• View post

  Following the rules today (updating a paper which was not written in the lipics format to use the lipics format)

• View post

  As a true ultrafinitist I believe all ultrafinitist theories. Therefore there cannot be a maximum number N due to the fact that there is an (N+1) ultrafinitist theory which I believe in

• View post

  > Some pull requests may be missing due to an ongoing search incident, but no data is lost. Use the API or GitHub CLI (gh pr list) for complete pull request results. Github is so cooked. I couldn't check the SampCert PR's yesterday and it looks like I can't check them today either