This article traces the 50-year history of proof assistants—software tools that help mathematicians and computer scientists construct and verify formal proofs. It covers key milestones from early systems like AUTOMATH in the 1960s through modern tools such as Isabelle, Coq, and Lean, highlighting how these systems evolved from niche research projects into powerful platforms now used in verifying software, hardware, and mathematical theorems.
A state-designed worm from 2005 called Fast16 sat undetected on VirusTotal for nearly a decade. It intercepted executable files at the kernel level and silently altered floating-point calculations in high-precision engineering software like LS-DYNA, which was used in Iran's nuclear weapons research. Unlike Stuxnet, Fast16 received little public attention for over twenty years.
Paul Graham reports that Y Combinator startups now have over 75% of their code written by AI, a threshold crossed at least one to two years ago. This parallels a similar transformation at Google, where AI-written code went from 0% to 75% in about two years.
Scientists are increasingly concerned about the potential collapse of the Atlantic Meridional Overturning Circulation (AMOC), a critical ocean current system. Such a collapse could have severe consequences for North America and Europe.
A compromised version of the LiteLLM Python package (version 1.82.8) was briefly available on PyPI, capable of exfiltrating sensitive credentials like SSH keys and cloud secrets. The malicious package affected any project that depended on LiteLLM, though it was only available for about an hour before discovery.
A supply chain attack has compromised the popular npm axios HTTP client library with 300 million weekly downloads. Malicious versions install a remote access trojan, though some users may have avoided infection through version pinning or older installations. Security experts warn this is a live compromise affecting one of npm's most depended-on packages.