Mastodawn

Jan 14

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.

Jan 14

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."

Jan 14

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 🤣

Jan 15

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.

Mar 13

Fenwick trees are dangerously fast, I propose we start researching A[i] xrisk

Mar 13

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)

Mar 16

HOW HARD COULD IT BE? 1000 lines and 15 hours of work later, now I know

Mar 16

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

Mar 24

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

Mar 24

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

Mar 24

Cleaned it up and will blog about it tonight 😃

Mar 25

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

Apr 10

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*

Apr 22

I hope someday they make a set-theoretic sequel to Piano Tiles called Peano Tiles

written in Lean ofc

I used to think ofc stood for "of f***ing course" and always wondered why people felt the need to swear in perfectly normal online situations

Mark Eichin Apr 22

@xy same. (Still do at first glance, it's a "*pause* oh right it's the other thing" correction rather than really believing it.)

1awawawa2awawawa Apr 22

@xy very nice of you

@xy does it not?

@LivInTheLookingGlass well at least for my own usage "wtf" and "ofc" stand for "what the fox" and "of foxing course" respectively

Yeah I know what {:isolate_assertions} actually does but it's funnier to view it as a silly magical line that makes your proof go blazingly fast 🚀

Apr 23

I bet a week later after learning more Lean I'm gonna come back and make a version with the roles swapped

Apr 24

Yay I proved my first "theorem" using Lean: the property lsb i ≤ i for the lsb function in Fenwick trees https://git.unnamed.website/leantest/tree/Main.lean?id=c86a44de06312ad58439038bec182efd2391e919#n41

But yeah it was excruciatingly hard since it was my first time without handholding from a book or guide but hopefully it'll get way easier over time.

Main.lean - leantest - Random Lean experiments

Apr 24

I think Lean and Dafny have rotted my brain... they're the only languages I take seriously nowadays, everything else just feels weak in comparison

Terence Tao: "Math can be very fragile: If one step in a proof is wrong, the whole argument can collapse. If you make a collaborative project with 100 people, you break your proof in 100 pieces and everybody contributes one. But if they don’t coordinate, the pieces might not fit properly. With proof assistants, you don’t need to trust the people you’re working with, because the program gives you this 100% guarantee."

So basically "Lean handles web scale you turn it on and it scales right up"

rdivyanshu Apr 24

@xy gestures xkcd 435

@rdivyanshu I apologize in advance for my ridiculously bad handwriting

OK I'll stop with the Lean propaganda

Apr 27

Wait this instance has a

custom emoji? Guess I have to add

and

as well then

I had to thickify the SVG for that

@xy DOUBTFUL

@xy 😅

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

I wonder if making all my Dafny/Lean/Fenwick-related posts in one giant tree causes perf problems...

Java 🤮:
public static void main()

Dafny 😃👍:
opaque twostate predicate main()

ML transformers 🤮

OCaml monad transformers 😀👍

Alright I made the https://lean.unnamed.website/ and https://btrfs.unnamed.website/ fan sites

You've heard of curl | bash but let's take it up a notch and do curl | sudo btrfs, what could possibly go wrong

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

May 8

I just tried unsafe Lean (analogous to unsafe Rust) and welp that crashed the Lean server several times

May 8

If I had to pick my favorite programming languages it would probably be:
1. Lean
2. Lean
3. Lean
4. Lean
5. Lean

Honorable mentions: Dafny, Julia

https://unnamed.website/posts/cosine-best-language-ever/

Yay I finally fixed the crashes and wrote a new blog post about #Lean!

Cosine in the BEST LANGUAGE EVER

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

Maybe I can improve it with some crazy dependent type stuff

"Had a bright future but started hanging out with some bad Idris kids."

May 26

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

May 7

LEAN RUNS ON 3 BILLION DEVICES EVEN MY PHONE

May 22

installed my favorite video game, Lean!

May 22

I wonder if I'm the first person ever to run Lean on a Nintendo Switch

May 23

Thanks to https://switchroot.org for making this possible!

switchroot

Switchroot is a group for open-source development on the Nintendo Switch, a Tegra X1-based game console with a FOSS bootstrap exploiting a low-level recovery bootloader.

May 22

Yes, this is a Kevin Buzzard reference

Whoa Rustan Leino mostly figured out the cause of my Dafny soundness bug: https://github.com/dafny-lang/dafny/pull/6208

Include rewrite antecedents in CanCall assumptions by RustanLeino · Pull Request #6208 · dafny-lang/dafny

Fixes #6158 This PR fixes an unsoundness that came about from a bad interaction between quantifier rewrites and CanCall assumptions. The need to rewrite quantifiers To describe the issue and the fi...

GitHub

1awawawa2awawawa Apr 22

@xy we have Peano Tiles at home
https://en.wikipedia.org/wiki/Peano_curve

Peano curve - Wikipedia

Right after a chapter on proving termination in Lean...

"Dictation software occasionally misunderstands "theorem prover" as "fear improver""

Apr 22

"Lean software development"? Nope, we're gonna try software engineering in Lean because why not!

Apr 22

Wait wtf this video game has an anime girl walkthrough on YouTube... yes, that's right, the internet will do that to any game, even the Lean Natural Number Game about formal proofs 🤣

Original Japanese version: https://www.youtube.com/watch?v=hazk0aVoJnU

Chinese sub: https://www.bilibili.com/video/BV16W4y1U7BT/?vd_source=a42206cdf86b7a82fc73aae3cc37d9de

(Couldn't find an English version sorry)

ゆかりんと茜ちゃんの証明ゲームLeanプレイ講座 #1【定理証明支援系】

YouTube

rdivyanshu Apr 20

@xy reading and playing with compfiles, better still formalizationing some toy but moderate complex mathematics problems and solutions in lean is how I *learnt to use* lean4