bollu

4 ms·

1.
by bollu 2mo ago
where would I learn a taxonomy of such motifs? I trained for classical piano as a kid, and I'm slowly trying to learn jazz piano as I ease back into it! I'd love to learn more about these types of harmonic ideas and motifs as I ge
2.
Show HN: Formally Verified FPSan(github.com)
2 points by bollu 3mo ago|0 comments
3.
by bollu 5mo ago
Lambda calculus talks about computable functions, where the types of the inputs are typically something discrete, like `Bool` or `Nat`. Here, the domain is the real numbers.
4.
by bollu 8mo ago
please send me an email <siddu.druid@gmail.com>. I'm a PhD student at cambridge, and might be able to put you in touch with folks who have positions to hire you as an RA if your research profile fits. even if there isn't an
5.
by bollu 9mo ago
how does one get to conversational level in a week? I would love to know!currently anki-flashcarding my way through italian...
6.
by bollu 9mo ago
Having similar reasoning, I would up writing a tiny-optimizing-compiler tutorial that only explains how to write a middle and back end of a compiler: https://github.com/bollu/tiny-optimising-compiler
7.
by bollu 11mo ago
That's really neat, I hadn't seen the black hole argument before, that's really cute
8.
by bollu 1y ago
yes, Lean is executable, and the proof of natural numbers runs with arbitrary width integers. they're stored as tagged pointers, with upto 63bit numbers being normal numbers, and larger numbers become GMP encoded.
9.
by bollu 2y ago
How does one formally define a spinor? I've seen the definition of a spinor field as "things that transform like a spinor", and a spinor as a "representation of the spin group" (which representation), but I would li
10.
by bollu 2y ago
How'd you recommend I learnt to paint? I've not really done much painting in my life at all, and I'd love a breakdown.
11.
Stuff I Learnt in 2024(pixel-druid.com)
2 points by bollu 2y ago|1 comments
12.
by bollu 2y ago
I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean ( https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%... ), and it's genius -
13.
by bollu 2y ago
Can you elaborate on the batching part for me? I don’t see it
14.
by bollu 2y ago
what definition of "fair" was reached upon?
15.
by bollu 2y ago
Nice! As someone who understands very little CSS, could you explain why this works?
16.
by bollu 2y ago
I've written about [this explanation of tensors]( https://pixel-druid.com/articles/tensor-is-a-thing-that-tran... ) before, and it seems worthwhile to write it down again: There are two ways of using linear maps in
17.
by bollu 2y ago
I am curious why you feel that way.
18.
by bollu 2y ago
Does the temperature actually change discontinuously in a physical system from -infty to +infty, or is it a theoretical artifact that does not show up experimentally?
19.
by bollu 2y ago
I have a very well documented implementation of rete, that also produces nice looking SVGs of the state of the rete algorithm here: https://github.com/bollu/rete It's a really interesting algorithm, and allows one
20.
by bollu 2y ago
Neat! do you have a resource that explains this perspective further?
21.
by bollu 2y ago
Yes, lilypond generates SVG that rescales smoothly
22.
by bollu 2y ago
You're right on one count: no library implements forward mode. Hence, you're correct that no autodiff library (including pytorch) implement autodiff this way. However, *you're wrong* that forward mode cannot be written in ter
23.
by bollu 3y ago
You are very wrong. Many of the key results of theoretical CS is to prove impossibility . There is no code to be written when you show that something is not possible. - Halting problem: impossibility of TM to determine if other TMs halt.
24.
by bollu 3y ago
Could you link to your code? I am interested in the API design of meshing a layout system with immediate mode GUIs
25.
by bollu 3y ago
How do you define the curvature for a cone when it has a singularity at the apex? From the definion that I know (angle defect), the tip of the cone will have curvature
26.
by bollu 3y ago
Surely you’re joking. Polya pioneered so much combinatorics I don’t even know where to begin. Heck, a lot of counting problems reduces to polya’s enumeration theorem. The page of “references” to stuff named after him should be a clue to y
27.
by bollu 3y ago
I am super confused. Why can't I take this purely classical circuit and run it on a classical computer? Somewhere, there should be some blowup into exponential time?
28.
by bollu 3y ago
I do not believe this. What will one do about intermetidate computations which can have complex coefficients? In general, you'd need some way to change the gates/ unitary matrices themselves to be purely real. So you'd need t
29.
by bollu 3y ago
Could you provide a link to some more reading about this? i do not know what a wada property is, nor why it is topological
30.
Stuff I Learnt in 2022(pixel-druid.com)
1 points by bollu 4y ago|0 comments

More ›