Show more

The Natural Number Game is in the process of being ported to Lean 4. A beta version is up and running on the web at adam.math.hhu.de/#/g/hhu-adam/.

Over the next two months there will be an intense period of development, with new worlds added like Even/Odd world and maybe prime number world. The game will be developed as one of my Xena summer projects. The Xena summer projects are where a bunch of undergraduates from across the world get together and make stuff in Lean. It's half in-person and half-online. More information on the Xena summer project website at github.com/kbuzzard/xena/blob/

The natural number game repo is at github.com/hhu-adam/NNG4. Suggestions (e.g. via issues) for additional worlds, bug reports etc are welcome!

I'm excited to play with the Open Book Abridged Edition. Thanks @joeycastillo for continuing to work on the Open Book project.

It's kind of delightful to pick up an object that tells you how to assemble it!

#OpenSource #OpenHardware

a bit too much meta for my taste 

Oh.
Kvadratisch, praktisch, nicht gut?

#Ritter Sport contiuing and even growing business in #russia.

leave-russia.org/ritter-sport

I know some stuff about it, including unmasking the author of the puzzle: boston.conman.org/2021/05/05

If someone wants to work on cracking this numbersstation, I would be glad to contribute.

Show thread

As I unfollowed someone who'd retooted one of their ads five or six times in the past day or so, and am seeing people both leave and talk about growing the Fediverse, I'm thinking about whether people are seeking parasocial or personal relationships from social media. And how much we lose when we're not clear on that distinction in our goals.

Speaking of odd websites.

Here's one: numbersstation.info/

I have managed to find the person who is behind it and wrote them an E-Mail. It seems like it's a challenge, but I'm yet to crack it.

There's an easy flag on my personal website: memorici.de

Actually, I make challenges for every website I make and put them there as easter eggs.

I want someone to get this particular one so bad.

The reason is that the challenge that I made for my personal website is also personal. It's a tale of an old friend who has passed, memories of teenage years and, really, the quintessence of the meaning behind the domain name.

As I said, I would rate this challenge as easy, in terms, it doesn't involve actual hacking or even API interactions, whereas the challenge that I put on doma.dev is likely to be hard or at least intermediate.

Good hunting, if you are up for it. And if you know of some random websites with flags, ping me.

CUSTODIAN CLEANUP ANNOUNCEMENT

We have put an instance-wide silence on two fediverse fuckwads, @stux and @supernovae, because they, as operators of large instances, are being dicks to .art, a much smaller instance, and are doing so in ways that raises all sorts of red flags, as they try to avoid taking responsibility for their own actions, and try to frame .art as the aggressor instead.

This moderation action will persist until the heat death of the universe, or until they stop being assholes.

Receipts;

en.wikipedia.org/wiki/DARVO

mstdn.social/@stux/11061209504

universeodon.com/@supernovae/1

mstdn.social/@stux/11057724191

dotart.blog/dotart-blog/defede

What is the hottest temperature you have experienced?

Please boost to increase sample size.

#ClimateChange
#ClimateCrisis
#climate

Viktor Orbán is Putin's Gauleiter, ruling over Russian ally Hungary.

Orbán says Putin is not a war criminal and Ukraine is not a sovereign country.

Hungary is a member of NATO and the EU and wield's Russia's veto in those bodies.

m.bild.de/politik/ausland/poli

I've licensed my posts CC-0, but sometimes I really want a different CC extension for social media

CC-SA-NA, NoAttribution, the opposite of BY, you must strip my username/PFP/any identifying information if you reshare.

CC-SA-PD, Plausible Deniability, you need to run the post through an LLM asking it to reformulate the post so it cannot be copy paste searched.

Haha, the guy wrote off russia as a "colonised" / "poorer" country on par with the African countries.

A bit of a joke given that russia steals gold and diamonds from Africa too.

Hopefully, unintentional.

Show thread

Thought I would start sharing some of the work I did for Kobold Press's Cities and Towns.
I really enjoyed working on this and Marc was a great art director.
AD: Marc Radle
#ttrpg #KoboldPress #Maps #DnD #battleMap #MastoArt #DigitalArt #ttrpgCommunity

Ukraine’s biggest enemy is the western belief that it cannot beat putin. Now is the time to rethink that

by Keir Giles

Extract
Until now, western backers have provided Ukraine with enough to survive but not to win. So, the Chatham House report concludes, the time is now to lift restrictions on the weapons systems supplied to Ukraine, and what #Ukraine can do with them, allowing Kyiv to achieve the defeat of russia that is essential for all our safety.

Read it here🔗 theguardian.com/commentisfree/

Shadow Lines, Cyprus DLR

Colour version of this shot. I purposely went out to capture photography of this lovely occurrence at Cyprus Docklands Light Railway station. I really love the dramatic shadows created by the architecture here!

#streetphotography #streetphoto #railway #photography #photographer #london #mastoart #art #underground #londonunderground #potd #tiling #shadows

A cryptobro DMed me to ask if I wanted to join his mailing list.

I spent slightly too long making this to send in reply.

QT: social.doma.dev/@goo/109922182

What we decided to do instead is to define two macros on the side. `defprod` is `defdata` that doesn't generate default constructors. It should be compatible with `defsum` out of the box, but we, for the time being, have the "no-new" counterpart called `defunion`.

Because unions are cool.

This way we don't break existing code, but allow easy to write smart constructors that don't upset .

The code is already live in the fork: github.com/doma-engineering/al

Show more
Doma Social

Mastodon server of https://doma.dev.