you...!!

the reason your body temperaure goes up when you're sick is that the viruses are using your body to mine crypto

i think any thoughts on programming languages delivered in the form of a youtube video can be dismissed by default

like were they actually stupid enough to believe openai would listen to anything they had to say or did they just show up to the roleplay sessions because it makes them feel important to give themselves a name that makes them sound like a regulatory body

did the people in the ai for math working group or wahtever it was called uhh. how do i put this. did they actually believe it?

(edit: the LARP troupe I'm referring to is the "The Advisory Group on Mathematics and Artificial Intelligence")

i log on. i:

• add fuel to a fire
• poke a bear
• open a can of worms
• stir a pot
• pour salt into a wound
• refuse to elaborate
• leave

apparently i don't talk enough about mikan! did you know…

• that mikan is somewhere between 60% and 70% faster than agda, if you allow filling in some implicit arguments that --lossy-unification is slow on?
• we can actually spell Type?
• mikan reports multiple type errors?
• mikan supports applying with-generated functions?
• we're experts on type theory and actually investigate the root causes behind consistency issues and implement comprehensive fixes, instead of proxying the output of one slop machine into the input box of another to produce brittle "fixes" that are overly specialised to the form of a reproducer?

by the way, if you would like some proof assistant branding that isn't slopped out corporate nonsense, i drew, by hand, some 88x31 buttons for mikan the other day. if you want to rep them on your website, you can hotlink them from me:

mikan flag mikan logo

or rehost them yourself. consider them CC BY-NC-SA; making the buttons link to https://codeberg.org/1lab/mikan constitutes "appropriate credit".

lmfao. this is how much of a shit the people maintaining your proof assistant give, apparently

slop poster reveals a certain class of person wants to be lean so bad it makes them look stupid

if scientists cared about advancing humanity they would be researching a way to reheat crispy foods without them going soggy

eagerly waiting to find out which neurotransmitter is going to ascend to the rank of fourth modern humour together with dopamine, serotonin and cortisol

y'all there's actually good news for once biologists in bolivia have described the first new species of felid in a century

google slop store

really the only innovation that we can credit the llm labs with is that they managed to invent a class of person even more annoying than evangelicals. the cult of the frontier model

HOLY SHIT!!!!!!!!!!!!!!!!!

AGENTIC-HAND-WRITTEN

"the real numbers"
🙅‍♀️ the
🙅‍♀️ real
🙅‍♀️ numbers

chat legit question it's probably a bad idea to have light text on dark background for your slides right

The decision to fork Mikan was not one taken lightly, by anyone involved with the project. Speaking personally, I know I would have rather continued to work with people whom I had looked up to in the past, whose writing was in many ways responsible for type theory being accessible and interesting to me in the first place, and indeed with some I had considered friends.

We're actually coming up to the fourth anniversary of my first commit to this repository; in this time, I had stepped up to maintain three completely orthogonal features, fixed bugs across literally every component other than the compilation backends, and implemented what is likely to be biggest performance improvement possible short of replacing the binary with exit(1); (parallel checking). All completely voluntarily, and, for the majority of that time, without making any demands. I was happy to do it! But when push came to shove, and I asked for what is ultimately a minor compromise for them weighed against explicit for what I believe to be an existential threat, the community landed somewhere between indifferent and getting chummy with self-admitted industry plants.

If the direction of the millenarian community effort is that of embracing whatever grift the soulless oligarchs in the Valley inflict on them, then far be it from me to jump in the way; there's only so many times I can get back up to keep working for the good of an academic pedigree and reputation whose supporting apparatus has taken every possible opportunity to reject my participation in any role beyond that of volunteer labourer, or perhaps "person who shows up to the pub". When standing in the golden halls of bird proof assistants, don't forget who was the janitor.

My ability to pressure anyone into switching implementations essentially ends with the 1Lab contributors, and it gives me great joy that they all stuck around, and even greater joy that a few heroes even stepped up to help with Mikan. They are also doing it voluntarily, and I am proud to have started projects that people can choose to contribute to, even despite my shortcomings.

The unfortunate reality, evidenced by the amount of correctness fixes we've done and performance wins we've pulled off, is that the bandwidth to maintain a proof assistant with seventeen hundred thousand different type theories does not exist anywhere on Earth. Dropping everything beyond what we use is not an attempt at hcomping my way into world domination. I simply believe formalisation is a joy, and I will not let that joy be taken away by people who believe in buying Thinking billed by the hour from the likes of Altman and Amodei.