platypii

Yea it's been fun! Everyone pretty much assumed n log n was the actual limit for integer multiplication. So the OpenAI result was surprising!

But of the 722 proofs openai released, integer multiplication did NOT come with a lean proof. So I wanted to see if the result was real, or maybe was a flaw in the proof. So I created the repo, and started burning tokens. It was not easy even with AI! It took a couple days laying the ground work. A huge part of the challenge was keeping the proof checking fast. It took ~8 hours for lean to check the first version of the proof. I fought to get it back down to ~20 minutes. Then huge credit to @jdb1729 for joining the effort and actually completing the proof across the finish line! The theorem was true!

Once we proved the initial openai bound of 2^-182, we've been working on integrating improvements to the bound, and we're now up to K = 2^-14. Continuing to work on it, community contributions welcome!

Sylvain Lesage’s cool interactive explainer on visualizing extreme row counts—think billions—inside the browser. His technical deep dive explains how the open-source library HighTable works around scrollbar limits by:

- Lazy loading - Virtual scrolling (allows millions of rows) - "Infinite Pixel Technique" (allows billions of rows)

Hyperparam sponsored Sylvain’s work as part of our broader effort to invest in open-source infrastructure and get ahead of the data-scale problems that are emerging with LLMs. With a regular table, you can view thousands of rows, but the browser breaks pretty quickly. We created HighTable with virtual scroll so you can see millions of rows, but that still wasn’t enough for massive unstructured datasets. What Sylvain has built virtualizes the virtual scroll so you can literally view billions of rows—all inside the browser. His write-up goes deep into the mechanics of building a ridiculously large-scale table component in react.

We're willing to spend money, but I've had the "datadog billing problem" before where it starts reasonable and then grows to a non-trivial percent of saas budget, and then theres a scramble to refactor. Trying to get ahead of that as the LLM logs are MUCH larger that my APM logs.

Makes sense. I'm not currently in snowflake because I'm mostly working with local parquet files. Would prefer not to have to pay for snowflake just to explore my data. I'm interested in better data UIs though so I might need to check it out.

I started Hyperparam one year ago because I knew that the world of data was changing, and existing tools like Python and Jupyter Notebooks were not built for the scale of LLM data. The weights of LLMs may be tensors, but the input and output of LLMs are massive piles of text.

No human has the patience to sift through all that text, so we need better tools to help us understand and analyze it. That's why I built Hyperparam to be the first tool specifically designed for working with LLM data at scale. No one else seemed to be solving this problem.