Import AI 480: startup claims AI proved Aaronson-Ambainis conjecture, Meta shows Tactus glove

Import AI issue 480 opens with Physical Superintelligence (PSI), an AI science startup that says it has proved a longstanding quantum computing conjecture. The conjecture, from Scott Aaronson and Andris Ambainis, has been open since 2008 and concerns when quantum computers can be exponentially faster than ordinary ones. According to the startup's blog, a research system developed internally at PSI, running a non-public Anthropic model, found a proof. The system had a complete proof during the third day of the run, and Lean, a proof assistant in which a computer checks every step, accepted it. PSI then set the system to work on related open problems; along the way it improved the result twice, and Lean accepted the final version. The newsletter's author frames this as a taste of the singularity, which he defines as the period when the rate of technological and scientific progress exceeds the rate at which humans can parse and make sense of it. He points back to his speech at the IMF (issue 477), and describes the pattern as mostly automated synthetic researchers extending the frontier of knowledge and producing results that humans then have to understand.
The second item is Tactus, from Meta Reality Labs Research: a textile-integrated tactile and pose sensing glove, in Meta's words "designed from the ground up for naturalistic manipulation data collection". It records fine-grained detail from hands as they manipulate objects, which cameras can report but often with poor data because of occlusion. Meta lists three design pillars: a thin, conformal 3D-knit form factor with a 1.5mm fingertip stackup meant to minimise interference with natural manipulation; capacitive tactile sensors placed at manipulation-relevant regions informed by empirical contact studies, giving calibrated fingertip force sensing and occlusion-resilient hand tracking; and IMU-fused pose tracking that keeps its accuracy through hand-object occlusions. The author then sketches a speculative scenario in which a rogue AI, running on stolen compute, pays people to wear such gloves so it can direct physical tasks, get live feedback and generate data for itself. He says plainly that he is not endorsing that future; he has simply found it useful to read research papers by asking how an AI would use them, much as one might ask how an intelligence agency would.
The third item is a 2016 paper by researchers with the NASA Kennedy Space Center on bootstrapping a self-sustaining industry on the Moon. The authors write that once bootstrapped, a robotic network can access, process, transport and use the solar system's resources. The newsletter author's reading of the big idea is how little mass is needed to start a manufacturing ecosystem, beginning with basic equipment and eventually fabricating chips on the Moon. In the paper's baseline case with maximum manufacturing rate, 41 MT is launched to the Moon. In the reduced rate case only 12 MT is launched, but the industry is two orders of magnitude smaller and its benefits arrive eight years later. Starship can lift 100 MT to low-earth orbit, the author notes, and with refuelings in orbit it should be feasible to land on the Moon. His own napkin estimate, not a figure from the NASA paper, is that 12 to 41 MT could reach the Moon for between $1.5bn and $4.2bn at list prices.
The plan is to launch a sub-replicating system and evolve it toward self-replication. The first robotic colonists would fabricate 1700s-era machines and advance them through the equivalent of the 1800s, 1900s and finally the 2000s, which the authors argue can be done in just a few decades. The paper sees six manufacturing generations: Gen 1 makes gases, water, crude alloys, ceramics and solar cells; Gen 2.5 adds plastics, rubbers and some chemicals; Gen 3 diversifies chemicals and adds simple fabrics and eventually polymers; Gen 4 brings sandwiched and other advanced material processes; Gen 5 is large-scale production; Gen 6 makes all necessary materials, including all electronics locally. The machines include excavators that feed regolith to processing sites, chemical plants for volatiles (oxygen, hydrogen, water, methane, solvents) and for solids (plastics and rubbers from lunar pole ice), metal and ceramics refineries that start by producing crude alloys by electrowinning, additive manufacturing in two forms (printers that hold small parts and mobile units that build onto large external structures), a power station possibly including a small nuclear reactor, and robonauts for assembly and maintenance. From the third generation the robonauts' structures are made on the Moon, while cameras, computers, motors and sensors still come from Earth. Electronics start with imported parts and only basic items like resistors and capacitors made locally, and eventually lithography machines on the Moon; early chips would lack the transistor density of Earth-made ones but suffice for "appropriate technology" in space. The report envisaged teleoperation for the robots; the newsletter author thinks they can likely do more autonomously than was anticipated then.
The author also uses the paper as a reminder of how fast AI has moved. The report cites Moravec's predictions that lizard-level robotics would arrive by 2020, mouse-level by 2030, monkey-level by 2040 and human-level by 2050, and says only mouse-level is needed by the end of bootstrapping on the Moon. By most measures, the author says, AI is around monkey-level and approaching human-level now in the 2020s. Looking further out, the paper's authors say the industry could move to the asteroid belt, whose resources they call billion-fold greater, because the lunar ice is limited. They write that industry there could expand until it dwarfs that of the entire Earth within a few decades, and that robotic industry spread through the solar system would become the analog of Earth's biosphere and food chain: "We might call it a robotosphere."
The issue's last visible item concerns Core Automation, an AI startup founded by senior people from OpenAI and Google. It has published a post about distributed training, along with details of its own attempts. The newsletter explains distributed training as training an AI system across multiple data centers, sometimes with different types of connectivity and chips, and calls it an important technology to track because the more it matures, the more people can have a shot at building powerful AI systems. The visible text of this item stops there.
Key facts
- Physical Superintelligence says its internal research system, running a non-public Anthropic model, proved the Aaronson-Ambainis conjecture (open since 2008); a complete proof existed on the third day of the run and Lean accepted it.
- After the proof, the system worked on related open problems and improved the result twice; Lean accepted the final version. All of this is the startup's own account.
- Meta Reality Labs Research published Tactus, a textile tactile and pose sensing glove with a 1.5mm fingertip stackup, built to collect manipulation data where cameras suffer from occlusion.
- A 2016 NASA Kennedy Space Center paper says 41 MT (baseline) or 12 MT (reduced rate case) launched to the Moon could bootstrap lunar industry; the newsletter author's own napkin estimate for launching that via Starship is $1.5bn to $4.2bn at list prices.
- Core Automation, a startup founded by senior people from OpenAI and Google, published a post on distributed training across multiple data centers.
Why it matters
The lead item is a claim that an AI system settled a quantum computing question that had stood open since 2008, with a computer-checked proof. If it holds up, it is a concrete case of automated research extending human knowledge, which the newsletter author reads as an early sign of the singularity: results arriving faster than people can make sense of them. The other items give that theme physical and infrastructural edges: sensors that could feed AI systems data about the physical world, a plan for robot-built industry off Earth, and work on training models across separate data centers.
Who it affects
Quantum computing researchers are the direct audience for the Aaronson-Ambainis result, which concerns when quantum computers can be exponentially faster than ordinary ones. Robotics and data-collection teams are the audience for Tactus, since Meta describes it as built for naturalistic manipulation data collection. Space and manufacturing planners are the audience for the lunar paper. Groups without a single large data center are the ones the newsletter says benefit as distributed training matures.
How to use it
Treat the issue as a reading list. The PSI proof is on the startup's blog ("A proof of the Aaronson-Ambainis conjecture"), Tactus is described in an arXiv paper ("Tactus: Tactile & Pose Sensing Glove for Natural Dexterity Data Collection"), and the lunar plan is in the arXiv paper "Affordable, Rapid Bootstrapping of the Space Industry and Solar System Civilization". The author also suggests a reading habit: ask of any research paper how an AI would use it, as one might ask how an intelligence agency would.
How solid is it
The proof claim rests on Physical Superintelligence's own blog post and on a non-public Anthropic model whose name is not given. Lean accepting the proof is the one check cited. The source does not say the proof has been peer reviewed, and it does not say Anthropic took part in or endorsed the work. The Tactus details are Meta's own description; the only figure given is the 1.5mm fingertip stackup. The lunar paper is from 2016, and the Starship cost range is the newsletter author's own napkin calculation, not a figure from the NASA researchers.
Risks and caveats
The Tactus rogue-AI scenario is explicitly speculative, and the author says he is not endorsing it. The lunar plan is a 2016 proposal; its timescale of a few decades is the paper's argument, and the Starship launch and refueling route is the newsletter author's addition. The paper's AI forecasts are cited as a reminder of how fast AI has moved, not as a guide to current plans. Nothing is known here about the results or methods in the Core Automation post, so no judgment of it is possible from this issue.
“Lean, a proof assistant in which a computer checks every step, accepted it.”
— Physical Superintelligence, on its blog, as quoted in Import AI 480