Leni Aniva
@aniva.bsky.social
🔧 Researcher in Machine Assisted Theorem Proving at https://centaur.stanford.edu/
☯️ Director of NorCal Hakkero Factory No. 1 (I make #touhou cosplay props)
🔗 https://leni.sh, https://pixelfed.social/chrysoberyl
❄️ Training AI on my content is prohibited
☯️ Director of NorCal Hakkero Factory No. 1 (I make #touhou cosplay props)
🔗 https://leni.sh, https://pixelfed.social/chrysoberyl
❄️ Training AI on my content is prohibited
「高槻」と「Palo Alto」とは同一意味ですか
January 27, 2026 at 1:19 AM
「高槻」と「Palo Alto」とは同一意味ですか
All Git repository tool configuration files (CI, issue template, etc.) should go in to `.config` like Cargo Nextest: nexte.st/docs/configu...
Currently we have .gitlab, .config, .cargo, ..., and it creates clutter.
Currently we have .gitlab, .config, .cargo, ..., and it creates clutter.
Configuring nextest - cargo-nextest
Configuring nextest: information about profiles and hierarchical configuration.
nexte.st
January 12, 2026 at 5:47 PM
All Git repository tool configuration files (CI, issue template, etc.) should go in to `.config` like Cargo Nextest: nexte.st/docs/configu...
Currently we have .gitlab, .config, .cargo, ..., and it creates clutter.
Currently we have .gitlab, .config, .cargo, ..., and it creates clutter.
Checkout the Touhou Zuhashichibun (東方頭破七分) videos in the description!
To learn more about the backstory behind this project, I traveled to Stanford to interview one of the instructors of the course! Check out the video here!
youtu.be/YdcnZD__IeI
youtu.be/YdcnZD__IeI
Cirno's Perfect Math Class in REAL LIFE | Touhou Hijack Field Club
YouTube video by Delta Pie
youtu.be
January 10, 2026 at 1:20 AM
Checkout the Touhou Zuhashichibun (東方頭破七分) videos in the description!
January 10, 2026 at 12:09 AM
After using Cadquery to make cosplay for 1.5 years I'm now moving away from it to #FreeCAD mainly because of:
1. Lack of interactive visualization tools. CQ-editor is fine but
2. Imports and visualization are incompatible with stl/obj files
3. Lack of integration with finite element solver
1. Lack of interactive visualization tools. CQ-editor is fine but
2. Imports and visualization are incompatible with stl/obj files
3. Lack of integration with finite element solver
January 5, 2026 at 12:17 AM
After using Cadquery to make cosplay for 1.5 years I'm now moving away from it to #FreeCAD mainly because of:
1. Lack of interactive visualization tools. CQ-editor is fine but
2. Imports and visualization are incompatible with stl/obj files
3. Lack of integration with finite element solver
1. Lack of interactive visualization tools. CQ-editor is fine but
2. Imports and visualization are incompatible with stl/obj files
3. Lack of integration with finite element solver
2026's main cosplay R&D Projects:
1. Toyosatomimi no Miko
2. Houjuu Nue (electromechanics)
3. Hijiri Byakuren's scroll (ITO thin film?)
1. Toyosatomimi no Miko
2. Houjuu Nue (electromechanics)
3. Hijiri Byakuren's scroll (ITO thin film?)
January 1, 2026 at 2:36 AM
2026's main cosplay R&D Projects:
1. Toyosatomimi no Miko
2. Houjuu Nue (electromechanics)
3. Hijiri Byakuren's scroll (ITO thin film?)
1. Toyosatomimi no Miko
2. Houjuu Nue (electromechanics)
3. Hijiri Byakuren's scroll (ITO thin film?)
A year ago, I saw the website of Yachie Lab (yachie-lab.org) at UBC and University of Osaka. It inspired me to make a cover page for my own website at leni.sh
December 30, 2025 at 12:33 AM
A year ago, I saw the website of Yachie Lab (yachie-lab.org) at UBC and University of Osaka. It inspired me to make a cover page for my own website at leni.sh
After the current MATP research is released, I'll post the #SuperSinography translations of some of the newly coined words.
今之機械定理証明研究(MATP)出版後、我意欲翻訳新発明之術語入#超漢文 。
例(Ex.): 探索視(Search View)
今之機械定理証明研究(MATP)出版後、我意欲翻訳新発明之術語入#超漢文 。
例(Ex.): 探索視(Search View)
December 13, 2025 at 8:06 AM
After the current MATP research is released, I'll post the #SuperSinography translations of some of the newly coined words.
今之機械定理証明研究(MATP)出版後、我意欲翻訳新発明之術語入#超漢文 。
例(Ex.): 探索視(Search View)
今之機械定理証明研究(MATP)出版後、我意欲翻訳新発明之術語入#超漢文 。
例(Ex.): 探索視(Search View)
December 8, 2025 at 9:19 AM
Found this gem on Youtube: m.youtube.com/watch?v=yrdy...
東方弾幕風で髙〇早苗の弾幕を作った
YouTube video by qwer
m.youtube.com
November 23, 2025 at 6:54 PM
Found this gem on Youtube: m.youtube.com/watch?v=yrdy...
Even research projects can be riced if you try hard enough
November 9, 2025 at 5:58 AM
Even research projects can be riced if you try hard enough
October 31, 2025 at 3:28 AM
Today, bots finally managed to overwhelm my tiny server at leni.sh and caused crashes on my Git server. It will be back online after further strengthening.
Leni Aniva
leni.sh
October 25, 2025 at 7:59 AM
Today, bots finally managed to overwhelm my tiny server at leni.sh and caused crashes on my Git server. It will be back online after further strengthening.
A user on Lean Zulip chat greeted me with "ciallo～(∠・ω<)⌒☆", so I replied to them with "Da★ze", but they did not respond.
October 17, 2025 at 3:54 AM
A user on Lean Zulip chat greeted me with "ciallo～(∠・ω<)⌒☆", so I replied to them with "Da★ze", but they did not respond.
If people want more frequent updates for my open source repositories they should consider helping me with cosplay. 🥲
October 14, 2025 at 5:23 AM
If people want more frequent updates for my open source repositories they should consider helping me with cosplay. 🥲
If anyone wants to write a relativistic bullet hell game I'm down to write the engine.
October 10, 2025 at 9:21 PM
If anyone wants to write a relativistic bullet hell game I'm down to write the engine.
To address the reproducibility crisis in computer science, I made codeberg.org/aniva/Manife... (also available on GitHub). Create reproducible #Nix builds for your #JuliaLang experiments!
Manifest2Nix.jl
A Nix library for building Julia Projects
codeberg.org
October 9, 2025 at 11:16 PM
To address the reproducibility crisis in computer science, I made codeberg.org/aniva/Manife... (also available on GitHub). Create reproducible #Nix builds for your #JuliaLang experiments!
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.
September 19, 2025 at 3:59 AM
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...
www.renaissancephilanthropy.org/gnn-smt-cons...
GNN-SMT consortium based proof automation for Lean 4 — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation
www.renaissancephilanthropy.org
September 17, 2025 at 9:14 AM
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...
www.renaissancephilanthropy.org/gnn-smt-cons...
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.
Concourse CI
concourse-ci.org
September 7, 2025 at 7:31 PM
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.