#lean
- skim rubik-lean4 and be reminded of On the nxnxn rubik’s cube[bonzio2018nxnxn] and Nxnxn rubik’s cubes and god’s number[salkinder2021nxnxn]
- skim read-lean

#gpu #os
- watch Coding Adventure: Optimizing a Ray Tracer (by building a BVH) and learn about the importance of BVH in ray tracing, and gkjohnson/three-mesh-bvh
- collect autodiff in GPU
- submit a bug report to Chromium
- thinking about separating devlog from reading diary
- thinking about turning my playground repos to monorepos by language/stack

#lean #sci
- found Teaching mathematics using lean and controlled natural language[massot2024teaching]
- noticed that Scientific Computing in Lean is now written in Verso!
- checked some progress in Type Checking in Lean 4
- I should put together a list of resources for learning Lean, as I have been asked and answered this question multiple times
- improve the VSCode Forester extension to have Hover, Go to definition, Search by title, and user-defined patterns for triggering completion

#bevy #os #rust #wasm #web
- add initial survey on headless render/testing for WebGL
    - Compiling C to WebAssembly without Emscripten and WebAssembly without Emscripten, a bit dead-end for me
    - found twr-wasm, a lightweight emscripten
    - I still need to learn more about wasmer and cranelift
- add test Rhai scripting
- learn about monorepo tools: nx seems to have most feature-complete support for most stacks, moon is the next best choice for Bun.js+Rust projects that I have in mind. Other resources:
    - Building a Monorepo with Rust
- I need to learn more about Salva: fluids simulation in Rust that works with Rapier, but it doesn't seem to have a JS binding yet, rapier even has an r3f package, and a plugin for bevy. See FLUID SIMULATION - SIGGRAPH 2007 Course Notes to learn more about fluid simulation.
- learn about WLJS for Wolfram Mathematica, recalled my early Mathematica notebooks, and wish to do SSR for them

#biome #web
- use `biome` for linting web source files
- add some links about Star Trek

#web #webgl
- add live reload
- improve various loading and WebGL animation experience
- found David Tong: Lectures on Gauge Theory

#gpu #render #shader #✍️
- more progress on Notes on ray-marching implicit surfaces, particularly on raymarching in raymarching (sphere tracing)
- found shaderfrog
- found three-gpu-pathtracer and related projects, particularly Physically Based Materials, and that Steve Trettel uses it to render black holes and Hopf fibrations
- found Multiview neural surface reconstruction by disentangling geometry and appearance[yariv2020multiview] (lioryariv/idr)

#os #quantum
- skimmed Geometric quantization[carosso2018geometric]: "Geometric quantization is an attempt at using the differential-geometric ingredients of classical phase spaces regarded as symplectic manifolds in order to define a corresponding quantum theory."
- skimmed Differential geometry: From elastic curves to willmore surfaces[pinkall2024differential]: "Unlike the common approach in existing textbooks on this topic, there is a strong focus on variational problems, ranging from elastic curves to surface that minimize area or Willmore functional."
- found demo-geodesic-heat and mesh-parameterize
- found From rings and modules to hopf algebras: One flew over the algebraist’s nest[broue2024rings]

#diagram #✍️
Make some progress on Notes on ray-marching implicit surfaces, particularly on mixing 4 elements (formulas, diagrams, algorithms, and readable working code).

#quantum
- skimmed The role of symmetry in the development of the standard model[love2024role] Cambridge lectures on the standard model[quevedo2024cambridge] Lectures on quantum mechanics for mathematics students[faddeev2009lectures] Quantum mechanics for mathematicians graduate studies in mathematics vol 95 (providence, RI: American mathematical society)[takhtajan2008quantum] Lectures on quantum mechanics for mathematicians[komech2019lectures], and The role of the rigged hilbert space in quantum mechanics[madrid2005role]

#bevy #cg #game #os #render #rust #shader #visualization
- found
  - symbolica for Rust and Python
  - Rusph: SPH algorithm in Rust for astrophysical simulations
  - Bevy: a game engine in Rust that could also be used for simulations
- looking for materials related to ray-marching with GA, found
  - Non-parametric realtime rendering of subspace objects in arbitrary geometric algebras[keninck2019non]
  - Exploring novel surface representations via an experimental ray-tracer in cga[hadfield2021exploring]
  - Real-time visualization of moebius transformations in space using quaternionic-bezier approach[karpavicius2013real]
  - Visualizing hyperbolic honeycombs[nelson2017visualizing] talk
  - pga3.glsl
  - Normals and the Inverse Transpose, Part 1: Grassmann Algebra in 2018

#apl #benchmark #compiler #gpu #os #render #rust #sci #shader #web
- found Compile Julia code to WebAssembly
- found SHADERed as another source of shader examples, particularly some are written in Rust, supported via one of its plugins
- looking for ways to include 3D models in LaTeX, found
  - asymptote
    - that can render .obj
    - that works in Overleaf
  - MeshLab that can export models to formats supported by media9
- watched Mike Seddon - Rust GPU Compute, found
  - Bend
  - faer-rs
  - cudarc
  - tinygrad
  - diol: benchmarking
  - wgpu-mm
    - Implementing Matrix Multiplication with WebGPU in Safari for optimized matrix multiplication on WebGPU
  - Fast CUDA SGEMM from Scratch
  - linfa: `scikit-learn` in Rust
  - gpu.cpp
  - CubeCL from Burn team
  - Candle from HF team
- read
  - WebGPU — All of the cores, none of the canvas
  - How to Optimize a CUDA Matmul Kernel for cuBLAS-like Performance: a Worklog
  - Autotune for GPU Kernels: Ensuring Consistent Peak Performance from Burn team
  - WebGPU Compute Shader Basics
- work through WebGPU Puzzles
- learned about APL and BQN
- a portion of The Dao Of FP
- learned about fpgatoy

#✍️
- make a start on Notes on ray-marching implicit surfaces
- make ray marching (naïve)

#os #shader
- trying to figure out curvature calculation in shaders
  - Screen Space Curvature Shader is a trick to mimic curvature calculation in shaders,using dFdx, dFdy in GLSL, Curvature shader by iY0Yi used it but it shows certain shower door effect
  - glsl-autodiff properly uses forward auto differentiation to calculate curvature in shaders, but it requires rewrite every math function for bookkeeping the gradient and the Hessian

#shader
- work out shader for test Keenan Crane's style for rendering edge and shade
- inspired by Surface Plotter (demo), read
  - Marching Cubes
  - Polygonising a scalar field
  - CIS700 Procedural Graphics: Implicit surfaces - Marching cubes
  - Marching Cubes Part 1: Explaining marching cubes

#formal #lean #optimization #os #rust #wasm
- add `egglog` and `ginac`, and streamline the build process of Rust WASM dependencies
- reading source of projects using egg: `jafioti/luminal`, `marcusrossel/lean-egg`, `verified-optimization/CvxLean` etc. TODO: read more egg papers: Bridging syntax and semantics of lean expressions in e-graphs[rossel2024bridging]An equality saturation tactic for lean[rossel2024equality]Verified reductions for optimization[bentkamp2023verified]

#gpu #render #web #z3
- mark candidates for rendering PDB: some links for viewing protein or molecules
- fail to run Z3 in browser (due to `SharedArrayBuffer` again)
- the source of examples of uwal and the corresponding articles at webgpufundamentals.org
- test compute.toys and test 3D Bifurcation Diagram

#shader
- Skim through Projective geometric algebra illuminated[lengyel2024foundations]
- experiments on compute shaders

#idea
- Polish Notes on Clifford Algebras
- Some more on translation of Bourbaki on Clifford algebras
- Re-skim Clifford and the ’square root’ ideas[trautman1997clifford]
- The algebra of grand unified theories[baez2010algebra] and make 97 notes
- Notes on Distributed Systems for Young Bloods (2013)

#formal #lean #sec #✍️
Ported the rest of the prelimilary part of The blueprint for formalizing geometric algebra in lean[wieser2024blueprint] to Notes on Clifford Algebras, except \(Z_2\)-graded derivations \(i_f\), anti-derivation
Make a start on notes on group algebras

#citation #idea #os
- The supergeometric algebra[hamilton2023supergeometric] and Unification of the four forces in the spin (11, 1) geometric algebra[hamilton2023unification]: illuminating path towards a unified theory of four fundamental forces, the first theory seemingly capable of reaching the same level of elegance and simplicity as A discrete model for gell-mann matrices[wilson2024discrete], the authors are also aware of potential issues and worked out viable solutions to address them. Unfortunately, there are no citations as of now.
  - Clifford and the ’square root’ ideas[trautman1997clifford] has certain historical remarks and a unusual approach that spinor representations are treated first for odd-dimensional spaces
spaces
- Geometry of lightning self-attention: Identifiability and dimension[henry2024geometry] (found on Mar 11, 2025 again)
- The tensor cookbook[ahle2024tensor] and Graphical tensor notation for interpretability
- The Calculus of Variations and Geometry: a Historical Perspective
- Data-driven linearization of dynamical systems
- Meta Flow Matching: Integrating Vector Fields on the Wasserstein Manifold

#cg #formal #physics #sci #sec
- [grassmann2000extension, ch. 1-4]
- [browne2012grassmann, sec. 1.1-2.8]
- The universe is not a lie, but actually an hopf, algebra[loret2024universe]
- some slides of AGACSE 2024
  - The Willing Kingdon Clifford Algebra Library
  - Look, Ma, No Matrices!
  - Spacetime Algebra and Octonions: Links with the groups used in particle physics and computer graphics
  - Construction of Exceptional Lie Algebra G2 and Non-Associative Algebras using Clifford Algebra
  - On Multidimensional Dirac-Hestenes Equation
  - On Rank of Multivectors in Geometric Algebra
  - From Null Monomials to Versors in Conformal Geometry
  - Look, Ma, No Trigonometry!
  - Dual Spaces are Real: Orientation Types in Geometric Algebras
  - On Generalized Degenerate Lipschitz and Spin Groups
  - Projective and Conformal Formulations of Electromagnetism
  - Representation and Gauge Freedom in Electromagnetism and Acoustics
  - Pencils and set operators in 3D CGA
  - Factorizations of the Conformal Villarceau Motion