#gpu #lean #rust
- Fish 4.0: The Fish Of Theseus, it's about Fish team porting Fish from C++ to Rust
- found cargo-gpu
- A letter to open-source maintainers
    - I hope to make a release for both GAlgebra and lean4_jupyter before or around the end of the year
- Dotfile Management using Stow
    - previously I was reluctant to use stow as it's written in Perl
    - maybe I'll also try `brew bundle` too

#rust #zig
- When Zig is safer and faster than Rust
    - and How to Actually Write C
- PKMs: Less Management, More Knowledge
    - found capacities and hoarder
- Gu Shi's *Möbius Continuum* and write a review on Weread

- found An introduction to universal artificial intelligence[hutter2024introduction]

- recieved pygae/galgebra#529 about Shirokov inverse, read On computing the determinant, other characteristic polynomial coefficients, and inverse in clifford algebras of arbitrary dimension[shirokov2021computing]

#os
- 🎿🪂
- reading Wang Guowei's philosophical works
- Ghostty Is Native—So What?

#news #os #proof #rust #✍️
- My Ph.D. advisor rewrote himself in bash, and learn about how weasel words, passive voice, and lexical illusions can make technical writing less precise, clear, and convey a lack of proofreading
- Playground Wisdom: Threads Beat Async/Await, and learn that in imperative programming, structured concurrency might be better than async/await, we don't always need to introduce functional programming concepts
- From where I left by antirez, the author of Redis, and learn that he likes the new license, and he does more work but better work by using AI to proofread and help testing the work instead of replace what he does better
- Fermat’s Last Theorem — how it’s going, and enjoy the story of finding the right work for fixing a fixable proof
- Dude, where's my main? and learn that executables can be position-independent just like libraries, and wonder if I can implement chaos engineering in Rust to learn more about low-level system design
- post-mortems for massive IT outage in recent years, and wish to keep a track of inspiring ones of them
- learn about git-backdate, which can help me date unpushed commits better

#agent #proof #software
- How wide is a proof?
- found Notes on Geometric Algebra
- skimmed Agents in software engineering: Survey, landscape, and vision[wang2024agents] and related papers

- 🚧 busy
- reading 📘*Zen and the Art of Motorcycle Maintenance: An Inquiry into Values*

#git #os #render #rust
- try Deepseek Deep Think, add deep think of Deepseek
- rethinking self-hosted git repos, CI, and pages, found
    - Forgejo
    - GitHub Pages App on Cloudron
- try using aider to write Rust script, not so good
    - based on an AoC Rust script example
    - try QwQ
- try copilot-more, maybe settle on it
- Clifford algebra or Lie algebra?
- learn a bit more about Slang, V, and Lobster
- watch Really amazing talk by Tomasz Stachowiak: Rendering Tiny Glades With Entirely Too Much Ray Marching
- The Door ProblemA from awesome-falsehood

#gpu #rust
- Optimizing a Rust GPU matmul kernel

#idea #quantum
- found
    - Knots inside fractals[broden2024knots]
    - Mathematical ideas and notions of quantum field theory[etingof2024mathematical]
    - Applied Linear Algebra and Differential Equations - Lecture notes for MATH 2350 by Jeffrey R. Chasnov
    - Competitive Programmer's Handbook

#haskell
- Haskell: A Great Procedural Language

- 🚧 busy

#os #shader
- found Slang
- Exploring Async Runtimes by Building our Own
- found The dirac equation in general relativity, a guide for calculations[collas2018dirac]

#compiler #vulkan
- found Impala
    - skimmed
        - AnyDSL: A partial evaluation framework for programming high-performance libraries[leissa2018anydsl]
        - RaTrace: Simple and efficient abstractions for BVH ray traversal algorithms[perard2017ratrace]
    - related:
        - shady
        - Vulkan Clang Compiler

#os
- skimmed
    - STAResNet: A network in spacetime algebra to solve maxwell’s PDEs[pepe2024staresnet]
    - A note on centralizers and twisted centralizers in clifford algebras[filimoshina2024note]

#citation #lean #os #rust #✍️
- experiments on using aider for LLM assisted project-level pair programming
    - this PR is a most extensive one
- finish citation trace for GAlgebra, see this PR for relevant readings
- found Towards a categorical foundation of deep learning: A survey[riccardo2024towards], Cat for DL
- found Cario, a provable Rust-like language

#os
- found Bartosz Ciechanowski's blog
- found Topics in differential geometry[michor2008topics] and Algebraic geometry[milne2012algebraic], helpful for Notes on Algebraic Geometry
- plan to read Templex-based dynamical units for a taxonomy of chaos[mosto2024templex]

#idea #lean #rust #wasm
- contemplate the idea of better file management with Rust
- meet datachain, extism, revisit mage-ai, should evaluate kestra, contemplate the idea of ML orchestration with Rust where each node is a WASM plugin, BAML has some potential
- wish to get back more on Lean and Math in this month

#compiler #idea #rust
- 🌴
- contemplate the idea of a bot to keep me going back to work on my projects, triggered by
    - an update of a related project
    - more than a month of inactivity
        - on the repo
        - or on a recent opened issue
- gccrs: An alternative compiler for Rust

#proof
- Isa Proof Shell

#git #gpu #neovim #ocaml #os #render #rust #shader
- Forester 5.x git log, not bumping to 5.x yet
- evaluate HTMX a bit
- Why not just embed Neovim?, will need to revisit Zed later
- RustGPU: Pros&Cons, the author becomes a maintainer of RustGPU
- found VR Schwarzschild black hole shader (works with SPS and SPS-I)

#✍️
- finish Notes on modern C++ programming

#benchmark #formal #rust #tui
- work on native-land
    - trying to make GA and math benchmark work, also evaluating the feasibility of benchmarking C++ libraries from Rust
    - pass CI on runpod
- work on formal-land, make Verso work
- debug various TUI tools

#formal #gpu #lean #neovim #rust
- work on native-land, trying to make rust-gpu fully work
- work on formal-land, trying to establish the infrastructure to explore multiple Lean 4 projects with independent toolchains and dependencies
- switching to Neovim, make it work for Rust, Lean, and forester
- write some useful key mappings in Neovim
- skim The Lean Language Reference
- start reading Modern C++ Programming Course (C++03/11/14/17/20/23/26)

#citation #haskell #physics #render #shader #vulkan #web #webgl
- initial citation trace for Gravitational lensing by spinning black holes in astrophysics, and in the movie interstellar[james2015gravitational] and Visualizing interstellar’s wormhole[james2015visualizing]
- Custom vulkan engine to render black holes in real time using ray-marching[meseguer2023custom] (Vulkan, Ray-marching, Kerr black hole) lrogerorrit/narwhalEngine
- Real-time high-quality rendering of non-rotating black holes[bruneton2020real] (CPU precal, WebGL2, Schwarzschild black hole) ebruneton/black_hole_shader
- skimmed Identifying black holes through space telescopes and deep learning[fang2024identifying]
- learn about Haskell-style type classes with isabelle/isar[haftmann2013haskell]: the type class for Isabelle, but its expressiveness is limited, see discussions in A construction of the lie algebra of a lie group in isabelle/HOL[schmoetten2024construction]

#benchmark #gpu #os
- Automatic differentiation: Inverse accumulation mode[siskind2019automatic] and A matrix-free exact newton method[naumann2024matrix], seems limited, but have some good references
- skim Gafro: Geometric algebra for robotics[low2023gafro] (good library and benchmark) and Developing GA-FuL: A generic wide-purpose library for computing with geometric algebra[eid2024developing] (good refs, but in C#)
- skim A comprehensive overview of GPU accelerated databases[sharma2024comprehensive], an interesting area with sparse tensors as an in-memory database in mind
- skim Felix: Optimizing tensor programs with gradient descent[zhao2024felix] (uiuc-arc/felix), which uses egg

#compiler
- found Functoriality in finitary vacuum einstein gravity and free yang-mills theories from an abstract differential geometric perspective[raptis2024functoriality]
- found A tensor algebra compiler for sparse differentiation[shaikhha2024tensor] and Felix: Optimizing tensor programs with gradient descent[zhao2024felix]
- SDQLite Optimizing tensor programs on flexible storage[schleich2023optimizing] (based on SDQL) is an intermediate language that expresses sparse tensor workloads by separating the tensoropt computations from the storage formats
- reminds me of A multi-level superoptimizer for tensor programs[wu2024multi]

#gpu
- work on native-land about GPU computation, see relavant README updates.

#bevy #game #idea #rust
- watch Chris Biscardi - Bevy: A case study in ergonomic Rust
- have a better idea about the game about fly, evade, slingshot, and shoot around black holes, 4D implicit surfaces
- explore sketchfab, polyhaven, and openverse, and have a basic idea about how to use them in the early stage of the game
- learn about itch.io to surveying existing games, and a open revenue sharing platform to release games
- found Algebraic geometry: A problem solving approach[garrity2013algebraic]

#lean #os
- C++ Package Managers: The Ultimate Roundup, and start using xrepo for C/C++ package management, it also supports a wide range of package repositories, including Conan, Conda, Vcpkg, Homebrew, Apt, and Cargo. But not BinaryBuilder.jl ecosystem (see also this FAQ).
- clarify the license for GinacLean, laying the ground for potential future work around Cadabra 2, which is licensed under GPLv3
- learn about Kento Okura's forest and Glade and Nota

#formal #gpu #lean #llvm #os #vulkan #web #z3
- add more plans in formal-land
- recovered Research Codebase Manifesto from Lean-MLIR
- recovered quotes from CICM 2020 Slack chat
- make CubeCL example work
- add CI with WebGPU on Mac & Ubuntu thanks to `llvmpipe`, `lavapipe`, `Vulkan SDK`, `Mesa` setup by tracel-ai/github-actions/setup-linux@v1
- found Lorenz and modular flows: a visual introduction

#news #os #rust
- learned about lobste.rs, a computing-focused community centered around link aggregation and discussion, a bit like Hacker News but less noise maybe
- Rewriting Rust and Josh Triplett's comment
- A multi-level superoptimizer for tensor programs[wu2024multi] and learn about mirage
- port My math interests in 2024
- make the Railscasts theme for Zed

#apl #os #tla #z3
- found ipe that is used extensively in tungsteno (source)
- Why I use TLA+ and not(TLA+), learn about PlusCal, Quint and Apalache (TLA+ to Z3)
- trying to figure out if TLA+ can be run in browser via TeaVM or CheerpJ

#os #render #web
- A simple approach to differentiable rendering of SDFs[wang2024simple]
- Rose: Composable autodiff for the interactive web[estep2024rose], and learn about Getting to the point: Index sets and parallelism-preserving autodiff for pointful array programming[paszke2021getting] dex-lang
- they are read on mobile app Reflow which has good PDF reflow support for math formulas in Arxiv papers, but not so good for other math book PDFs

#category #game #idea
- learn about catcolab.org and double category
- learn about Curved Diffusion: A Generative Model With Optical Geometry Control from ECCV 2024
- Reusing Styles from Tailwind CSS, decide to use it for CSS refactor
- found vanjs, considering for using it for VDOM and SSR
- learn about the game sgued/slingshot (just like a recent idea about black hole puzzle game inspired by Star Trek: Discovery)

#os #render #rust #sci #shader
- Differentiable Programming
    - found Differentiable Programming for Image Processing and Deep Learning in Halide and gradient-halide autodiff for halide
    - Adelta: Automatic Differentiation for Discontinuous Programs for A𝛿: Autodiff for Discontinuous Programs – Applied to Shaders Aδ: Autodiff for discontinuous programs-applied to shaders[yang2022delta]
    - found Dr.Jit
    - found Stan Math Library
    - found Kokkos
    - should eval the Rust crates of Rose
- found mistral.rs for LLM inference, which uses a HF candle fork internally
- found Why is anything conscious?[bennett2024anything]

#render #rust #shader
- found A simple approach to differentiable rendering of SDFs[wang2024simple] and Interval shading: Using mesh shaders to generate shading intervals for volume rendering[tricard2024interval]
- work on Rust stuff, particularly read about dioxus

#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

The readings during this period are reflected in

- some links for rendering implicit surfaces
- some links for learning shaders

Many experiments on Forester are done, as summarized in A customizable, hybrid approach to code & resource pipeline and embedding.

The readings during this period are yet to be reflected in Notes on Algebraic Geometry.

The readings during this period are reflected in Notes on Topos Theory and Type Theory.

translation of Bourbaki on Clifford algebras was ported to Forester on 07-22.

The readings during this period are reflected in Compendium on Spin groups. Some are yet to be reflected in Notes on Hopf Algebras.

#os
The readings during this period are reflected in

- My math interests in 2024
- Studying group algebras with GAP
- Notes on Zeon Algebra