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.
Initial citation trace for Gravitational lensing by spinning black holes in astrophysics, and in the movie interstellar[james2015gravitational] and Visualizing interstellar’s wormhole[james2015visualizing].
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.
Skim Gafro: Geometric algebra for robotics[low2023gafro], a good library and benchmark, and Developing GA-FuL: A generic wide-purpose library for computing with geometric algebra[eid2024developing], with good references 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], which uses egg.