Analog Fractals

All the images in this video are created by video feedback only – no computers are involved. The upper and lower monitors both display the same thing – the image from the camera, which is looking at the upper monitor. This creates a video feedback loop. It’s a delicate art to operate the device, an interplay between the camera and monitors, the position of the monitors, and the monitor control dials (hue, saturation, brightness and contrast). Doing controlled feedback like this requires these control dials, but most HD TVs and monitors don’t have analog knobs like old CRT TVs did, making it difficult to create controlled feedback in HD.

50% more Food

Humans have an enzyme called FTO that demethylates N6-methyladenosine through oxidation. It’s part of a large family of enzymes that do this sort of thing using an iron atom in their active sites, along with molecular oxygen. Plants, though, don’t have an FTO homolog – they have some other enzymes that can demethylate this substrate, but not like FTO itself. So the team behind this paper wanted to see what would happen if you engineered the FTO enzyme into plants. In rice and potatoes, the crop yields went up by 50%. Grain size in the rice plants didn’t change, nor did the height of the plants – they just produced a lot more rice grains in general. How does this happen? The plants’ root systems were deeper and more extensive, and photosynthetic efficiency went up by a startling 36%. Transpiration from the leaves was up 78%, but at the same time, the plants of both species showed significantly higher drought tolerance. These are highly desirable traits, and it’s worth noting that a lot of this extra biomass is coming from increased usage of carbon dioxide from the air.

Now we just need to crush the GMO luddites to roll this out.

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.

Doggerland

500m wide, the beach is made of material dredged from the sea bottom 13 kilometers offshore and dumped on the existing beach. It’s an experimental coastal protection measure, its sands designed to spread over time to shield the Dutch coast from sea-level rise. The endeavor has made 21m cubic meters of Stone Age soil accessible to archaeologists. “The surprising thing is just how much DNA is still down there.”

2022-03-06: A map of Doggerland 11 ka BP:

Doggerland was, by any estimation, the most attractive landscape in northwestern Europe for Mesolithic hunter-gatherers and perhaps the continent’s most densely populated region at the time. Because of the seemingly inexhaustible resources present there, normally mobile Mesolithic societies may have been encouraged to create permanent or semipermanent settlements. While relatively few Mesolithic sites have been located on land, if Doggerland was indeed the heartland for these early Holocene communities, it stands to reason that many archaeological sites may lie beneath the North Sea. Seismic data has now given archaeologists a much better sense of Doggerland’s topography. They know where its rivers, lakes, and coastlines were located, and where its forests were found. They can use this information to speculate about where people may have lived.
This new type of research into Doggerland has the potential to once again dramatically alter the field of European prehistory. “We have a completely intact landscape with a state of preservation that we can often only dream of on land. I think we will have a lot of exciting discoveries to come. We are barely scratching the surface.”

Transhuman Olympics

Throughout repeated attempts at reform, one thing has become clear: the IOC will not save us. It is an institution rotten to its core, and incapable of serious change. Rather than more protests and petitions. It’s now time to exit. I recommend a new kind of Olympics without the World Anti-Doping Agency. In short, I propose an Olympics with no drug testing. Incremental improvements to the current state of drug testing are simply not an attainable solution. The notion of anti-doping as a path to fairness must be abandoned entirely. Instead, we should celebrate a drug-enabled Olympics that would outcompete the original in terms of viewership, athletic accomplishment, and cultural legitimacy. The Transhuman Olympics would do more than improve the playing field for international athletics. It would sublimate geopolitical rivalries into a competition that is not merely harmless, but actually productive. In essence, leveraging the popularity and notoriety of the Olympics as a way to fund development into improved pharmaceuticals, alongside improved equipment, prosthetics, and medicine with general prosocial uses. The true aim however, is even more basic and foundational. We need to remind humanity that progress is still possible. Not by mere milliseconds and millimeters, but by literal leaps and bounds. We need to demonstrate decisively over and over again that human civilization is improving on undeniable axes. And we need to do it in a public arena.

Facebook Metaverse

No one company will run the metaverse — it will be an “embodied internet”, operated by many different players in a decentralized way. So, one is you will be able to, with basically a snap of your fingers, pull up your perfect workstation. So anywhere you go, you can walk into a Starbucks, you can sit down, you can be drinking your coffee and kind of wave your hands and you can have basically as many monitors as you want, all set up, whatever size you want them to be, all preconfigured to the way you had it when you were at your home before. And you can just bring that with you wherever you want. If you want to talk to someone, you’re working through a problem, instead of just calling them on the phone, they can teleport in, and then they can see all the context that you have. They can see your 5 monitors, or whatever it is, and the documents or all the windows of code that you have, or a 3D model that you’re working on. And they can stand next to you and interact, and then in a blink they can teleport back to where they were and kind of be in a separate place.

Cockatoo Culture

Even when residents in these areas weigh down the tops of their bins with bricks or stones, cockatoos have figured out how to knock these heavy objects to the ground. Once that barrier is removed, the hungry birds can crack the lid open with their beak, prop it on their heads and walk it back until it fully flips on its hinges, as the videos show below. This unique skill has now become so widespread in Sydney, researchers think the parrots are imitating and learning from one another – a sign of cultural evolution.

400 ka Knowledge Exchange

Different groups of hominins probably learned from one another much earlier than was previously thought, and that knowledge was also distributed much further. A study on the use of fire shows that 400 ka ago knowledge and skills must already have been exchanged via social networks. The most important question is: what was it that made widespread cultural diffusion possible 400 ka ago? ‘I hope we can change the discussion surrounding fire use by hominins. That we look more at what the use of fire meant for human development and how that related to social change.’

Jurassic Pompeii

The misfortune that struck this place 167 ma BP has delivered to him an extraordinary collection of fossil animals in what is unquestionably one of the most important Jurassic dig sites ever discovered in the UK. The quantities involved are astonishing. 10Ks of these animals that scientists collectively call “the echinoderms”. It’s a great name, derived from the Greek for “hedgehog”, or “spiny”, “skin”. What is a sea urchin, if not an “underwater hedgehog”? But it’s also the quality of the preservation that’s jaw-dropping. Lean in close to a slab of rock that’s just been cleaned up and you’ll observe what, at first sight, reminds you of a plate of noodles. It is in fact a great mass of fossil arms from who knows how many sea lilies. You can clearly discern the individual calcite plates, or ossicles, that made up the skeletal frames of these animals when they were alive. What’s more, the specimens are fully articulated. Everything is captured in 3 dimensions.

2023-05-13: And a similar site also in the UK

Fossils from 462 ma BP recently discovered in a quarry, called Castle Bank in central Wales reveal some Cambrian life forms held on for millions of years longer than paleontologists had thought before going extinct, and certain classes of modern animals got their starts earlier than expected. The quarry also holds strange creatures thought to have arisen and vanished during the Cambrian period, such as opabiniids, which had five eyes and a long proboscis, and scaly slugs called wiwaxiids. Newcomers spotted in the deposits include modern families of glass sponges and a group of crustaceans called horseshoe shrimp, which were thought to have arisen much later. The researchers have found 170 species. “There is every reason to expect that the diversity of the fauna will continue to climb as the authors continue their research”. But even the currently documented diversity emphasizes the underappreciated importance of this time, called the Ordovician, which set the stage for the world’s current biodiversity. The Welsh quarry could definitely be as famous as the Burgess Shale.