This year, we setup a booth for people to play #Touhou at Stanford Festifall.

Why is Youtube removing all the old 東方頭破七分 and 東方恐露西亜 Audio MADs? Even ロシアのパーフェクト政治教室 is gone. At this rate I'll have to build a mirror repository for all these videos.

We at centaur.stanford.edu are excited to share that our #matp proposal was selected to receive funding through the 1st round of the AI for Math Fund by @renphil21.bsky.social ! www.renaissancephilanthropy.org/gnn-smt-cons...

uhhh

Happy Cirno day!

With great difficulty, I, LightQuantum, and @stepbrobd.com have successfully packaged a #concourseci (concourse-ci.org) service into #NixOS along with accompanying examples. Tutorial incoming after changes.

Aeroponics is another field I feel could greatly benefit from open source (3D print schematics, parameters, controllers), but the open source schematics I found are meh...

A tutorial about setting up a #selfhosted declarative #nix #forgejo server: leni.sh/post/250901-...

I'm breaking up the cosplay monorepo at git.leni.sh/aniva/Cosplay into the newly created NHF1 homepage: codeberg.org/NHF, where we will have separate repos for infrastructure and designs. There will also be tooling for clothing drafting. Stay tuned!

Last time I went to Tokyo, I saw a lot of nice clothes that I can't get in North America, but many of them have fake pockets which really irritates me. This kind of manufacturer corner cutting (and cosplay) is what motivates me to learn pattern drafting and sewing.

Remaking #yasakakanako 's onbashira's bearing disk mechanism after accidentally breaking the previous one. See details here leni.sh/post/250708-... #cosplay

www.tomshardware.com/software/pro... Time to move to #Codeberg! codeberg.org/aniva

One the main concerns about modern AI is that the black-box nature of these models may lead to malicious ("misaligned") actions. To me the solution is to explore alternative architectures and eventually retire LLMs. However this faces the obstacle that LLMs have siphoned away most research funding.

I'm fed up with the drafting software Valentina. Parametric drafting should not be this hard. I'll write my own drafting software with Blender.

今になってこの人はCS99の訪問者の半分を引き付けた

I drew a new cover art for my research page! I have not given her a name, but the character on the left is my #OC (see avatar). #vectorart #silhouette #inkscape

Please board: No service

My thoughts on the crucial importance of methodology on self-reported AI performance on mathematics competitions, and my policy on commenting on such reports going forward: mathstodon.xyz/@tao/1148814...

#leanlang #research leni.sh/post/250720-...

#leanlang 's CSLib design slides are here: docs.google.com/presentation... Hopefully this doesn't become another design-by-committee project.

I'll be an area chair at the AI4Math workshop this Friday at #ICML 2025 in Vancouver: sites.google.com/view/ai4math...

Laser-cut pins for the 15th anniversary of #badapple. Made by myself. #touhou

#badapple animation inside #Blender 's Node Editor www.youtube.com/watch?v=C49Z...

Many MATP startups have reached out to have me drop out and join them. I declined, but they don't know that it is (not only) because I won't have time and resources to cosplay if I go into industry.

How I made the parametric #cosplay for #yasakakanako #touhou leni.sh/post/250708-...

New svg-based #isometric cover image for leni.sh

Anyone can write code that runs. Only a software engineer can write code that barely runs.

I have backported Pantograph, the #lean4 #matp machine-to-machine interaction tool, to #leanlang v4.9.0. This provides new features for people who wish to use older datasets. github.com/stanford-cen...

Machine Gun Kanako #touhoufest #touhou #cosplay #東方Project This set won a judge's favourite award

A machine gun in an onbashira for Yasaka Kanako #touhou #cosplay #yasakakanako #東方Project #cosplayprops

Excited to see #LeanLang in the new @stanforduniversity.bsky.social course CS99: 𝘍𝘶𝘯𝘤𝘵𝘪𝘰𝘯𝘢𝘭 𝘗𝘳𝘰𝘨𝘳𝘢𝘮𝘮𝘪𝘯𝘨 𝘢𝘯𝘥 𝘛𝘩𝘦𝘰𝘳𝘦𝘮 𝘗𝘳𝘰𝘷𝘪𝘯𝘨 𝘪𝘯 𝘓𝘦𝘢𝘯 4, by @aniva.bsky.social, Abdalrhman Mohamed and sponsored by Clark Barrett, including fantastic slides and #LeanLang code! See the course: web.stanford.edu/class/cs99

Hi all! I'm still alive and will be hosting a Touhou hijack panel at @touhoufest.org! I'll be going into why Touhou hijacks keep happening and some of the cool things I've discovered over my years of researching hijacks. Hope to see you there!

#touhou #cosplay #shikieiki

#cosplay #touhou Shiki Eiki Yamaxanadu's crown designed using Gauss' Theorema Egregium. Source code: git.leni.sh/aniva/Cospla...

When I finish all the Julia probabilistic programming things I'll make a relativistic Touhou-like game where spacetime could be not flat and there would be Lorentz transforms based on the characters velocity.

I wish our lab's website looked like this: yachie-lab.org?lang=EN

To this day I don't consult LLMs for any of my tasks. I've seen a worrying trend of researchers becoming dependent on LLMs for engineering problems and it significantly shortened their attention span, and they couldn't solve problems that the LLMs don't know.

The Perfect Math Class is coming this spring! I'll be the instructor of the newly created Stanford #lean course CS99, covering from functional programming and mathematics to meta-programming. See perfect-math-class.leni.sh

First board art of Stanford CoDa building! #touhou #cirno

Does anyone use #pixelfed? After the Meta AI fiasco I want to migrate all my cosplay engineering content to some other platform. pixelfed.social/chrysoberyl

Somehow got on a Japanese newspaper, but I told the journalist I came here because of 東方Project and it wasn't included ):

I went to Shinano-machi (信濃町) to cosplay as Airmoto-san. #今夜は砕頭 !

Everyone saw this coming

When I first entered the field of Machine Assisted Theorem Proving (MATP, some call it AI4Math, ATP, ITP, etc.), almost nobody was interested in this field, but now it seems like every AI researcher wants a dab at it.

Time to visit Suwako's home shrine with her

The more I think about the Page curve in Black Hole thermodynamics, the more it seems like a laundry machine full of socks. As you pull socks out of the machine they are initially "random", but as more socks come out they become paired up outside of the machine. www.researchgate.net/figure/Page-...

#SMT solvers have applications from verification to model checking. This is a graphical explanation of SMT solver's Conflict-Driven Clause Learning (CDCL) and Model-Based Quantifier Instantiation (MBQI) algorithms: leni.sh/post/informa...

I have added a few new features to #lean4 proof automation tool Pantograph git.leni.sh/aniva/Pantog... in response of user request, and will merge them by the end of the week. These includes goal/environment state pickling, type error extraction, and constant extraction. #AcademicSky #PhDSky

First coined by the Aesop paper for #lean4 proof automation, Metavariable Coupling is a phenomenon occurring during automated reasoning that complicates proof search. I wrote an article (first of many) here leni.sh/post/informa... to explain the effect and methods of mitigation. #AcademicSky #PhDSky