#git #interop #lean #os
- found pyonji, a tool to support sr.ht style e-mail patches
- Git: programmatic staging
    - and learn about `grepdiff`, unfortunately, it's not available on Mac
    - `git add -p` is also acceptable for a small number of hunks
- MathML with Pandoc
- Starting on seamless C++ interop in jank
- found Anemll: Artificial Neural Engine Machine Learning Library

#formal #os #web
- DeepSeek-prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition[ren2025deepseekproverv2]
    - A survey on post-training of large language models[tie2025survey]
        - notes on LM could be based on this survey and the following papers related to r1
    - 100 days after DeepSeek-R1: A survey on replication studies and more directions for reasoning language models[zhang2025days]
        - Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning[guo2025deepseek]
            - should revisit
    - found critics of r1/GRPO
        - Understanding r1-zero-like training: A critical perspective[liu2025understanding]
        - Does reinforcement learning really incentivize reasoning capacity in LLMs beyond the base model?[yue2025does]
    - Kimina-prover preview: Towards large formal reasoning models with reinforcement learning[wang2025kimina]
- found A Survey of Interactive Generative Video
- Polishing your typography with line height units
- Solving Sudoku with Algebraic Geometry and Computer Algebra : A C Programming Approach

#apl #formal #lean #os #prolog
- found Leanabell-prover: Posttraining scaling in formal reasoning[zhang2025leanabell]
- skimmed Flow matching guide and code[lipman2024flow]
- APL: Comparison with Traditional Mathematics
- I use Zip Bombs to Protect my Server
- found Prolog Notes
- found Quotes on notation design & how it affects thought

#agent #os #✍️
- found A Dependently Typed Assembly Language
- Qwen3: Think Deeper, Act Faster
- found Topologies and Sheaves Appeared as Syntax and Semantics of Natural Language (2012)
    - reveals connection between sheaf theory and linguistics
- found On the expressivity role of LayerNorm in transformers’ attention[brody2023expressivity] [code]
- found Grammar prompting for domain-specific language generation with large language models[wang2023grammar]
- wrote My setup with 4 screens and 2 Macs

#compiler #llvm #os #zig
- BitNet v2: Native 4-bit Activations with Hadamard Transformation for 1-bit LLMs
- Converting a C API to Zig with the help of comptime
- How a Single Line Of Code Could Brick Your iPhone
- found Nouveau: The Rule Based Language Family
    - and easily got into an infinite loop by adding a rule trying to combine a match and a box back to a matchbox
- Technical Debt as Theory Building and Practice
- Using HAProxy to protect me from scrapers
- What if we embraced simulation-driven development?
    - Notes about ETCD, there are some war stories
    - Notes about Raft's paper
- toycalculator, an MLIR/LLVM compiler experiment.