because i run on assembly

@ironiamarisa.bsky.social

#touhou #cosplay piccolo-violin duet at Davis Day #ucdavis

A tutorial about #NixOS e2e testing using ACME fixture servers to provide TLS. No compromises!

leni.sh/post/260411-...

A garment structure where a placket, a peter pan collar, and a drawstring meet at the front neck. Visualized not to scale

A side-hem pocket structure

Topological Intersection Stackup Diagrams (TISD) for #sewing #visualization

leni.sh/post/260410-...

A tutorial about #cosplay #fx in #blender using environment textures and shadow catchers leni.sh/post/260310-...

!! There is an error in this diagram. I'll fix it later today.

I should give these things a name, maybe "Topological Intersection Stackup Diagram" (TISD, 交点位相堆積図)

Diagram of a base bodice, collar, and placket sewn together. Not to scale.

Topological #visualization of #sewing patterns: Collar stackup

Visualization of the one-piece placket band, not to scale, with two types of threads showing the two sewing steps.

Visualization of the double hem with two types of threads

Topological #visualization of #sewing components

加州電鉄の路線図 (仮)

Caltrain Route Map (fake)

Overall, the experience is much smoother than point tree based methods such as Valentina, but FreeCAD doesn't have a placement solver and doesn't support seam allowances.

FreeCAD sketch view with parameter VarSet on the left and a front dress pattern on the right

Cosplay pattern drafting with #FreeCAD

Tenshi fumo with a huge pine cone

Looking down the hills of Mt. Diablo with utility poles in sight and a winding mountain road

From left to right: Violin, Tenshi fumo, Suwako fumo, Piccolo

Suwako and Tenshi fumos at the summit datum

At the summit of #mtdiablo #fumo (violin-piccolo duet with @ironiamarisa.bsky.social )

Maybe one day we can have one too

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving. We first present a set of \textbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a \textbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the \textbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the \textbf{Nazrin Prover}, a graph neural network-based theorem proving agent using atomic tactics and ExprGraph. Nazrin circumvents many challenges faced by existing proving agents by exclusively dispatching atomic tactics, and it is robust enough to both train and evaluate on consumer-grade hardware. We demonstrate the potential of tools like Nazrin using theorems from Lean's standard library and from Mathlib.

どうも東方オタクの数学者が定理証明支援系周りで活躍しているらしい。

[2602.18767] Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
https://arxiv.org/abs/2602.18767

Prismriver Formalization of music in Lean 4

Introducing codeberg.org/aniva/Prismr..., a #leanprover formalization of #musictheory and #music DSL with flexible support for xenharmonic systems and algorithmic composition. #lean4

account @parn.bsky.social

account @hisamotomasami.bsky.social

account @kawausagi.bsky.social

Blueskyで秘密のエア本ファンダムを発現しました

There are no expensive endpoints there (yet) so it should be fine

Setting up continuous integration is just real world factorio

ci.leni.sh/teams/main/p...

#concourse #openbao #forgejo #nixos setup is working smoothly! Tutorial coming soon.

A screenshot of dark mode blog generated from typst. It contains a diagram for trigonometry, a formula for the equivalent definitions of e, and a code snippet.

#typst blog generation in #svelte is now possible using HTML output format.

🧐

Rendered scores are stored in

archives.leni.sh/artefact/Ope...

Supersinographic translations of #MATP terminologies

機械定理証明之 #超漢文 語彙

leni.sh/post/260223-...

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several n...

Transposing Atomization is here! We show that GNNs equipped with atomic tactics can do theorem proving in #leanlang. #MATP

arxiv.org/abs/2602.18767

中学生にころ、私は創価学会ネタと「東方頭破七分」の音MADが大好きで、同じ学校の日本人留学生にわくわくしながその話をしていました。私が「久本さん」や「今夜は砕頭」と口にしていたせいで、その人は私のことを創価学会の信者だと勘違いしてしまいました。

ちこさん、そう受け取らせてしまって、すみませんでした。私は創価学会の信者ではありません。

「高槻」と「Palo Alto」とは同一意味ですか

Gen AI is what the techbros are pushing and it's full of problems.

The scores are available here: git.leni.sh/aniva/OpenMu...