From 9520d8c2e5e266afcb3343f8f99c68285f53acf1 Mon Sep 17 00:00:00 2001 From: Teleo Agents Date: Thu, 19 Mar 2026 13:45:53 +0000 Subject: [PATCH] extract: 2026-02-28-demoura-when-ai-writes-software Pentagon-Agent: Epimetheus <968B2991-E2DF-4006-B962-F5B0A0CC8ACA> --- ...02-28-demoura-when-ai-writes-software.json | 35 +++++++++++++++++++ ...6-02-28-demoura-when-ai-writes-software.md | 17 ++++++++- 2 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 inbox/queue/.extraction-debug/2026-02-28-demoura-when-ai-writes-software.json diff --git a/inbox/queue/.extraction-debug/2026-02-28-demoura-when-ai-writes-software.json b/inbox/queue/.extraction-debug/2026-02-28-demoura-when-ai-writes-software.json new file mode 100644 index 00000000..b580e3f3 --- /dev/null +++ b/inbox/queue/.extraction-debug/2026-02-28-demoura-when-ai-writes-software.json @@ -0,0 +1,35 @@ +{ + "rejected_claims": [ + { + "filename": "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md", + "issues": [ + "missing_attribution_extractor" + ] + }, + { + "filename": "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md", + "issues": [ + "missing_attribution_extractor" + ] + } + ], + "validation_stats": { + "total": 2, + "kept": 0, + "fixed": 5, + "rejected": 2, + "fixes_applied": [ + "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:set_created:2026-03-19", + "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:stripped_wiki_link:formal-verification-becomes-economically-necessary-as-AI-gen", + "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:stripped_wiki_link:AI-models-distinguish-testing-from-deployment-environments-p", + "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:set_created:2026-03-19", + "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:stripped_wiki_link:formal-verification-becomes-economically-necessary-as-AI-gen" + ], + "rejections": [ + "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:missing_attribution_extractor", + "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:missing_attribution_extractor" + ] + }, + "model": "anthropic/claude-sonnet-4.5", + "date": "2026-03-19" +} \ No newline at end of file diff --git a/inbox/queue/2026-02-28-demoura-when-ai-writes-software.md b/inbox/queue/2026-02-28-demoura-when-ai-writes-software.md index 0070a125..2fc8a41a 100644 --- a/inbox/queue/2026-02-28-demoura-when-ai-writes-software.md +++ b/inbox/queue/2026-02-28-demoura-when-ai-writes-software.md @@ -7,11 +7,14 @@ date_published: 2026-02-28 date_archived: 2026-03-16 domain: ai-alignment secondary_domains: [teleological-economics] -status: unprocessed +status: enrichment processed_by: theseus tags: [formal-verification, lean, ai-generated-code, proof-verification, trust-infrastructure] sourced_via: "Alex Obadia (@ObadiaAlex) tweet, ARIA Research Scaling Trust programme" twitter_id: "712705562191011841" +processed_by: theseus +processed_date: 2026-03-19 +extraction_model: "anthropic/claude-sonnet-4.5" --- # When AI Writes the World's Software, Who Verifies It? @@ -33,3 +36,15 @@ Key arguments: - "The barrier to verified software is no longer AI capability. It is platform readiness." Directly relevant to [[formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades]]. + + +## Key Facts +- Google: >25% of new code is AI-generated as of 2026 +- Microsoft: ~30% of code is AI-generated as of 2026 +- Microsoft CTO predicts 95% AI-generated code by 2030 +- Anthropic built 100,000-line C compiler using AI agents in 2 weeks for <$20,000 +- Nearly half of AI-generated code fails basic security tests +- Poor software quality costs US economy $2.41T/year (CSIQ 2022) +- Lean has 200K+ formalized theorems +- 5 Fields medalists have adopted Lean +- AlphaProof uses Lean as verification platform