Tag: software

Web Photoshop

This has to be some kind of high water mark for web capabilities. Pretty late in the game, unclear that it matters much? For example, will WebAssembly take full advantage of Apple custom silicon?

Over the last 3 years, Chrome has been working to empower web applications that want to push the boundaries of what’s possible in the browser. 1 such web application has been Photoshop. The idea of running software as complex as Photoshop directly in the browser would have been hard to imagine just a few years ago. However, by using various new standardized web technologies, Adobe has now brought a public beta of Photoshop to the web.

0.001% Mathlib

When Lean came out, there were plenty of other proof assistants available, including Coq, which is the most similar to Lean — the logical foundations of both programs are based on dependent type theory. But Lean represented a chance to start fresh. Mathematicians created mathlib and eagerly began to fill it with the world’s mathematical knowledge. The work has the air of a barn raising. “If you were to quantify how much of mathematics is formalized, I’d say it’s way less than 0.001%.” It will probably take decades before mathlib has the content of an actual research library, but Lean users have shown that such a comprehensive catalog is at least possible — that getting there is merely a matter of programming in all the math. Last year, the Lean community put aside the accumulation of undergraduate math and skipped ahead to the vanguard of the field. The goal was to define one of the great innovations of 21st-century mathematics — an object called a perfectoid space that was developed over the last 10 years by Peter Scholze. In 2018, the work earned Scholze the Fields Medal.

This project just hit a major milestone, as Peter Scholze explains:

While this challenge has not been completed yet, I am excited to announce that the Experiment has verified the entire part of the argument that I was unsure about. I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research. Congratulations to everyone involved in the formalization!!

In this Q&A-style blog post, I want to reflect on my experience watching this experiment.

How did the formalization proceed?
Initially, I imagined that the first step would be that a group of people study the whole proof in detail and write up a heavily digested version, broken up into many many small lemmas, and only afterwards start the formalization of each individual lemma. This is not what happened. Instead, the formalization followed quite closely the original lecture notes, and directly attacked Lemma after Lemma there. It did seem that the process was to directly type the proofs into Lean. Lean actually gives the user a very clear summary of what the current goal is, so one always needs to get a very clear sense of what the next few steps really are. Sometimes it was then realized that even on paper it does not seem clear how to proceed, and the issue was brought to attention in the chat, where it was usually quickly resolved. Only after a lemma was entirely formalized, the proof, now thoroughly digested, was again written up in the Blueprint in human readable form.

What did you learn about the process of formalization?
I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.

see also this earlier piece about using coq:

For 10 years, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes”. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. The real potential of type theory informed by homotopy theory is as a new foundation for mathematics that’s uniquely well-suited both to computerized verification and to studying higher-order relationships.

and even earlier efforts:

A grand objective of the field is to formalize the whole of mathematics, reproving its theorems with a negligible probability of error, all based on a small kernel (in the HOL Light system, the kernel is 500 lines of OCaml code).

and another backgrounder

As the towering mathematical enterprise reaches new heights, with more intricately and esoterically turreted peaks, each practitioner drilling down into minutiae that could never be understood by colleagues even in the same field, computers will be necessary for advancing the enterprise, and authenticating the integrity of the structure—a structure so complex in detail and so massive in scale that adjudication by mere human referee will no longer be feasible

one person’s perspective

I’m not concerned by the fact that no human mathematician can check this, because we can check it with other computer approaches

2023-06-01: Progress continues, and now LLM have entered the picture

We set out to tackle serious mathematics with a combination of hope and trepidation. We were able to formalize everything we set out to formalize and were never forced to discard a development part way through. “We have formalized results by 2 Fields medalists (Roth and Gowers), an Abel prize winner (Szemerédi) and of course Erdős too!” We’ve also seen impressive advances in search and language models to assist users in proof development. Although the effort required to formalize mathematical articles remains high, we can confidently predict that formalization will be playing a significant role in mathematical research in the next few years.

2025-09-11: Gauss

Using Gauss we produced ~25K lines of Lean code, comprising 1K theorems and definitions. Formal proofs of this scale have historically been major milestones, often the culmination of multi-year efforts. The largest singular formalization projects in history — career-defining efforts, which can span more than a decade — are only an order of magnitude larger at up to 500K LOC. Lean’s standard mathematical library, Mathlib, is 1 OOM beyond that, at 2M LOC, comprising 350K Lean theorems and definitions, and developed by 600 human contributors over 8 years. With further algorithmic improvements, we aim to increase the sum total of formal code by 2-3 OOM in the coming 12 months. This will serve as the training ground for a new paradigm — verified superintelligence and the machine polymaths that will power it.

Destroying Cellebrite

By a truly unbelievable coincidence, I was recently out for a walk when I saw a small package fall off a truck ahead of me. As I got closer, the dull enterprise typeface slowly came into focus: Cellebrite. Inside, we found the latest versions of the Cellebrite software, a hardware dongle designed to prevent piracy (tells you something about their customers I guess!), and a bizarrely large number of cable adapters.

By including a specially formatted but otherwise innocuous file in an app on a device that is then scanned by Cellebrite, it’s possible to execute code that modifies not just the Cellebrite report being created in that scan, but also all previous and future generated Cellebrite reports from all previously scanned devices and all future scanned devices in any arbitrary way (inserting or removing text, email, photos, contacts, files, or any other data), with no detectable timestamp changes or checksum failures. This could even be done at random, and would seriously call the data integrity of Cellebrite’s reports into question.

Any app could contain such a file, and until Cellebrite is able to accurately repair all vulnerabilities in its software with extremely high confidence, the only remedy a Cellebrite user has is to not scan devices. In completely unrelated news, upcoming versions of Signal will be periodically fetching files to place in app storage. These files are never used for anything inside Signal and never interact with Signal software or data, but they look nice, and aesthetics are important in software. Files will only be returned for accounts that have been active installs for some time already, and only probabilistically in low % based on phone number sharding. We have a few different versions of files that we think are aesthetically pleasing, and will iterate through those slowly over time. There is no other significance to these files.

LOOPY

In a world filled with ever-more-complex technological, sociological, ecological, political & economic systems… a tool to make interactive simulations may not be that much help. But it can certainly try.

play with simulations
It’s the ancient, time-honored way of learning: messing around and seeing what happens. Play with simulations to ask “what if” questions, and get an intuition for how the system works!

programming by drawing
Raw code is too inaccessible. Also drag-and-drop is too mainstream. But with LOOPY, you can model systems by simply drawing circles & arrows, like a wee baby

remix others’ simulations
Want to build upon your friends’ models? Or challenge your enemies’ models? LOOPY lets you have a conversation with simulations! You can go from thinking in systems, to talking in systems

Fastest PNG Decoder

Wuffs’ PNG image decoder is memory-safe but can also clock between 1.22x and 2.75x faster than libpng, the widely used open source C implementation. It’s also faster than the libspng, lodepng and stb_image C libraries as well as the most popular Go and Rust PNG libraries. High performance is achieved by SIMD-acceleration, 8-byte wide input and copies when bit-twiddling and zlib-decompressing the entire image all-at-once (into 1 large intermediate buffer) instead of 1 row at a time (into smaller, reusable buffers). All-at-once requires more intermediate memory but allows substantially more of the image to be decoded in the zlib-decompressor’s fastest code paths.

Citi $900m mistake

Last August, Citigroup Inc. wired $900M to some hedge funds by accident. Then it sent a note to the hedge funds saying, oops, sorry about that, please send us the money back. Some did. Others preferred to keep the money. Citi sued them. Yesterday Citi lost, and they got to keep the money. I read the opinion, expecting to learn about the New York legal doctrine of finders keepers—more technically, the “discharge-for-value defense”—and I was not disappointed. But I was also treated to a gothic horror story about software design. I had nightmares all night about checking the wrong boxes on the computer.

See, the “don’t actually send the money” box next to “PRINCIPAL” is checked, but that doesn’t do anything, you have to check 2 other boxes to make it not actually send the money.

Malleable Systems Collective

  1. Software must be as easy to change as it is to use it.
  2. All layers, from the user interface through functionality to the data within, must support arbitrary recombination and reuse in new environments.
  3. Tools should strive to be easy to begin working with but still have lots of open-ended potential.
  4. People of all experience levels must be able to retain ownership and control.
  5. Recombined workflows and experiences must be freely sharable with others.
  6. Modifying a system should happen in the context of use, rather than through some separate development toolchain and skill set.

ML bank interconnect

Stripe uses ML to improve transaction success rates by 10%

Over time, that model will learn in specificity, for a particular bank in middle America vis their UK-homed customers who have typed in lower cased zip codes, that the bank strongly prefers upper casing zip codes. So we just do that for them, for transactions across our network

Werner Vogels

The 8 services were really just the fundamental pieces to get, put, and manage incoming traffic. Most importantly, there are so many different tenets that come with S3, but durability, of course, trumps everything. The 11 9s (99.999999999%) that we promise our customers by replicating over 3 availability zones was unique. Most of our customers, if they have on-premises systems—if they’re lucky—can store 2 objects in the same data center, which gives them 4 9s. If they’re really good, they may have 2 data centers and actually know how to replicate over 2 data centers, and that gives them 5 9s. But 11 9’s, in terms of durability, is just unparalleled. And it trumps everything.

learnings from scaling AWS