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 index b580e3f3..caf8722f 100644 --- 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 @@ -1,33 +1,24 @@ { "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", + "filename": "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md", "issues": [ "missing_attribution_extractor" ] } ], "validation_stats": { - "total": 2, + "total": 1, "kept": 0, - "fixed": 5, - "rejected": 2, + "fixed": 3, + "rejected": 1, "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" + "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md:set_created:2026-03-19", + "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md:stripped_wiki_link:formal-verification-becomes-economically-necessary-as-AI-gen", + "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md:stripped_wiki_link:formal-verification-of-AI-generated-proofs-provides-scalable" ], "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" + "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md:missing_attribution_extractor" ] }, "model": "anthropic/claude-sonnet-4.5", 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 2fc8a41a..2729b994 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 @@ -15,6 +15,9 @@ twitter_id: "712705562191011841" processed_by: theseus processed_date: 2026-03-19 extraction_model: "anthropic/claude-sonnet-4.5" +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? @@ -48,3 +51,16 @@ Directly relevant to [[formal verification of AI-generated proofs provides scala - Lean has 200K+ formalized theorems - 5 Fields medalists have adopted Lean - AlphaProof uses Lean as verification platform + + +## 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 +- Morrison (Lean FRO) demonstrated AI-generated Lean implementation of zlib with mathematical proof