A retrospective on five decades of proof assistant development, from early pioneers like Automath and LCF to modern systems such as Isabelle, Coq, and Lean. The article traces the evolution of interactive theorem proving, highlighting key milestones in logic, automation, and formal verification that have shaped today's mature proof assistant ecosystem.
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.