Plugins for those who care

A Tale of Two Machines

Blank Canvas GBA Game: online | .gba file | taptap.io

Game Boy Advance J-RPG game about an artist who struggles with making a first brush stroke on a blank canvas during the white nights in St. Petersburg. She visits places of importance to her, gets involved into unlikely conversations, fights her own demons, until finally — [sorry, no spoilers]

Formalizing stuff in pure Lean

• Core FST theory, axiom-of-choice-free, no Mathlib
• MV-algebras + proof systems for Łukasiewicz logic and Hájek's Basic Logic, axiom-of-choice-free, no Mathlib



• What next? Who knows.