I wrote a fast Fenwick tree library for my flash cards app: https://git.unnamed.website/sdc/tree/fenwick.c

The operation "Search for largest index with prefix sum less than or equal to s" isn't a common thing that people do with Fenwick trees so I had to read an arXiv paper about it.

The nice thing about Fenwick trees is that they're only a few lines of code but... on the other hand they use crazy incomprehensive bit hacks!

fenwick.c - sdc - C port of SD, a very efficient flash cards app

I haven't done benchmarks to confirm this, but Fenwick trees should use 1/4 the memory of segtrees and be somewhat faster since they use for loops and bit hacks instead of recursion.
The other weird thing about the "search for largest index with prefix sum less than or equal to s" operation is that it views the Fenwick array as an implicit binary tree while the update and query ops view the array as (two different) binomial trees. So maybe the tagline for Fenwick trees should be "One array. Three trees."
And here's a Fenwick the squirrel who I folded 1.5 years ago. I guess his name is because he lives in a Fenwick tree or something. When I folded him last year, I told my friends there was a squirrel in my room and they thought a real squirrel was running around wrecking havok in my room 🤣

Welp, somehow I gaslighted myself into thinking that squirrel's name was Fenwick. It's actually Segtree and the real Fenwick is a rabbit.

Anyways, today my friend Isaac (https://slightknack.dev) convinced me to organize my random Fenwick tree ramblings into a blog post and he also drew a nice diagram for my post! https://unnamed.website/posts/fenwick-trees-awesome/

Featuring fake calculus, insane Python programs, and one liner bit hacks!

Home — Isaac Clayton

A cozy little corner of the web.

Fenwick trees are dangerously fast, I propose we start researching A[i] xrisk
Hmmm maybe I should try formally verifying my Fenwick trees post using Dafny... it's only 5 lines of code, how hard could it be?? (top words said before major disasters)
HOW HARD COULD IT BE? 1000 lines and 15 hours of work later, now I know
New (absurdly long and insane) blog post about formally verifying Fenwick trees using Dafny, feat. Kublai the camel, Fenwick the rabbit, SHL the fox, and a proof of 0 == 1! https://unnamed.website/posts/formally-verifying-fenwick-trees/
Formally Verifying Fenwick Trees

Formally verifying the Fenwick tree data structure using Dafny and Kublai the camel

I severely underestimated the difficulty of the challenge problems I posed at the end of that blog post...

What I expected:
★☆☆ <15 minutes
★★☆ <1 hour
★★★ <3 hours

In reality:
★☆☆ <1 hour
★★☆ eh it'll take an afternoon
★★★ DO NOT ATTEMPT

I'm trying to challenge 5: "Implement prefix search and prove it." and I wrote a 100 line Dafny proof but it's so nasty and hacky that I don't wanna ever post that monstrosity on my blog
Cleaned it up and will blog about it tonight 😃
New sequel to my formally verifying Fenwick trees post, feat. Kublai, using Dafny in #Rust, and more proofs: https://unnamed.website/posts/actually-useful-formal-verification/
Doing Something Actually Useful With Formal Verification

Using my formally verified Fenwick trees library for a flash cards app in Rust

Another new post in my Fenwick trees/Dafny series! This time I proved the time complexity of Fenwick trees: https://unnamed.website/posts/proving-fenwick-trees-fast/
Proving That Fenwick Trees are Fast

Using Dafny to formally verify the time complexity of Fenwick trees

I have a particularly nasty Dafny proof that the reverse of the reverse of a linked list is the list itself: 158 lines of pure pain. Should I write it up as a blog post, or is it too scary?

Learning Lean right now and I think Dafny seriously spoiled me since it was a struggle even to define the lsb function from my Fenwick post:

def lsb (i : Nat) : Nat :=
if i == 0 then 0 else if i % 2 == 1 then 1 else 2 * lsb (i / 2)
termination_by i
decreasing_by
cases i
· simp
contradiction
· simp_all [Nat.div_lt_self]

grinding the Lean game https://adam.math.hhu.de/#/g/leanprover-community/nng4 right now, tbh it's a bit boring since I know all these things would be trivial to do in Dafny

Yay finally finished in 150 minutes, other than the Fermat's Last Theorem level!

Sadly, I still have no idea how to use Lean 4.

Someone needs to make a crossover of the Lean Natural Number Game and Touhou
Help I really succ at this game... *intense peano music intensifies*
I hope someday they make a set-theoretic sequel to Piano Tiles called Peano Tiles
written in Lean ofc
I bet a week later after learning more Lean I'm gonna come back and make a version with the roles swapped
Wait TIL the same guy created both Z3 and Lean, and Dafny is just "throw everything into Z3 and hope for the best" so maybe it's not Lean VS Dafny it's Lean ❤️ Dafny
Not only does Lean feel like the Rust of proof assistants, it literally *is* Rust: a Lean dev said "Our inofficial fallback design heuristic is "if we don't know what to do, do it like Rust"." and elan is the same code as rustup just with 's/rustup/elan/g' 's/cargo/lake/g' 's/rustc/lean/g'
I hope this makes the Rust fans try Lean
I should make some fan sites sometime:
- btrfs fan site where the entire site is just a btrfs send-ed file that you can btrfs receive
- Dafny fan site with a large gallery of proofs of false
- Lean fan site with an animified version of the natural number game
- Ali's fan site wait no that already exists that's just my current website
Honestly I'm starting to prefer the live interactivity of Lean over Jupyter notebooks (no hidden state!) (but Pluto.jl of course will forever still be my favorite)

I just realized I've been learning Lean for a few weeks now and I've just never compiled any of my programs since if you know the program is provably correct why would you ever run it? (Yeah I know I've made that joke a million times but it's kinda true)

Anyways I'm running `lake build` for the first time and it's compiling hundreds of mathlib stuff weeeeeeee

I just tried unsafe Lean (analogous to unsafe Rust) and welp that crashed the Lean server several times
Yay I finally fixed the crashes and wrote a new blog post about #Lean https://unnamed.website/posts/cosine-best-language-ever/
Cosine in the BEST LANGUAGE EVER

How to implement the lazy infinite power series trick in unsafe Lean

Another blog post about #Lean: https://unnamed.website/posts/doing-math-with-lean/

This time I proved

$\sum_{n=2}^{\infty} \sum_{p=2}^{\infty} \frac{1}{n^p} = 1$

Doing Math With Lean

Using Lean to prove a double summation identity