Bartosz Naskręcki

live-workshop-skill. Claude Code skill: Turn any lecture into a structured, searchable knowledge base with live Whisper transcription

eml-formalization. Lean 4 + Mathlib formalization of arXiv:2603.21852 (Odrzywołek, EML)

12puzzle. This project contains a complete proof of the isomorphism of the symmetry group of the 12-puzzle and the full symmetric group S_12.

threecyclegen. Fix three positive integers n, k, m Prove that a group subgroup H of S_{6+(n+k+m)} generated by g1:=G!(1,6,4,3,a_1,...a_n); g2:=G!(1,2,4,5,b_1,...,b_k); g3:=G!(5,6,2,3,c_1,...,c_m); H:=sub<G|[g1,g2,g3]>; satisfies H = S_{6+(n+k+m)} or H = A_{6+(n+k+m)}.

fineqs. Lean4 formalization with Artistotle of the arXiv paper 1906.11174

impress. HTML

symm. TypeScript

isogeny_genus_2. Independent Magma and SageMath verification of arXiv:2606.02429

math-ai-mirages-2026. Lecture, evidence ledger, formal artifacts, and reproducible companion on AI for mathematics (MIM UW, 22 June 2026)

leiden-declaration-tracker. Knowledge base tracking every internet mention of the Leiden Declaration on AI and Mathematics (leidendeclaration.ai) — 131 verified mentions across 127 outlets and ~15 languages.