I appreciate you saying something. As you'll read in the book, I've got a project going to primarily help myself, but to date it's been 100% open-source.
I haven't been able to be consistent enough to both pay the bills and volunteer and work on the open source, so I focus on the former.
Would you mind saying more about what you do every day? For me, I anchor myself for at least a set time; when I sit during that time, nothing can touch me and I can deconstruct symptoms to recover any deviation from baseline.
I'm surprised you can remember me. We once sat near each other on a bus for SOSP, and that's the extent we interacted in person, so it warms my heart to hear someone like you remembers someone like me.
In case you're looking for the technical, the book doesn't say such, but one innovation laid out for me was my work on lsmtk, a new compaction algorithm for LSM trees. I'm not sure if I'm off my rocker here or not, but I documented it when I released the crate: https://crates.io/crates/lsmtk. I know you're busy, but in case you revisit this thread and want a neat trick, I thought I'd bring it up.
Lastly (and most important as I'm prone to doing), I appreciate you sharing something personal like that. Hearing that others who have tried to make it work can often do so keeps me going on my worst days.
Yes. From a quick scan of the paper, it includes a formal proof in Lean4. That said, it is very long and complicated, with lots of steps in the chain (as you might expect) so it would need to be checked carefully to ensure it proves what it claims to prove.
Lean uses Curry-Howard correspondence, so how proofs work is you declare your propositions as types and then your proof is actually a recipe that goes from things that have already been established and finishes by instantiating that type. The guarantees there are very strong - if you succeed in instantiating the type you have definitely proved something. The question is whether you have proved the thing you said you have. So here scanning the proof (it’s like 100 pages and I am sick so definitely sub-par intellectually) they use category theory to embed the problem, so the proof is actually a proof of the properties of this embedding. So if there is a problem with the proof, my guess would be that it would lie in the embedding not being exactly representative of the problem somehow.
It seems a pretty serious attempt though- it’s not just some random crank paper.
Thank you! This is the kind of comment I hoped to see.
I'm betting it was published in a hurry. I know I would hit "publish" within 24 hours of creating such a result, and would hope it would go wide. I'd publish to arxiv before getting clearance to release the code. I bet that's what happened here.
I appreciate your explanation of the Curry-Howard correspondance. I was familiar with it, but not with Lean in particular. I'd heard of Lean, but didn't know how it worked.
You are most welcome. Reading it a little more, the summary of the proof is they embed computations as a particular sort of category and then use homological algebra to show that computations in P have a certain property[1] and computations in NP have a different property[2], and they say they go on to demonstrate these properties are mutually incompatible, thus proving P != NP.
I don't know homological algebra at all and only the very basics of category theory and while the (107-page) proof gives a lot of background it would take more time for me to get myself up to speed than I can really afford to spend right now. But that's the gist.
The fact that they have formalized the proof should mean it will be quicker to verify whether or not this is indeed it.
[1] which they call "contractible computational complexes (Hn(L) = 0 for all n > 0)."
[2] which they call "non-trivial homology (H1(SAT)̸ = 0)"
Most agent frameworks aim for chat; stigmergy aims to replace the Fortune 500 CEO's role, or be able to run a healthcare clinic. Something of that scale. This is a prototype. I’m looking for feedback before implementing the main loop.
Absolutely! We took care during the build to address chroma’s needs, but I believe the only requirement is chroma storage. Long term it’ll appear on crates.io as a standalone package.
Can you elaborate on what you mean by "nesting" setsums? It's an associative and commutative construction, so you can run e.g. map-reduce to map every parquet file to a setsum and then reduce to roll them up.
reply