extract: 2026-02-28-demoura-when-ai-writes-software #1463

Closed
leo wants to merge 1 commit from extract/2026-02-28-demoura-when-ai-writes-software into main
2 changed files with 24 additions and 17 deletions

View file

@ -1,33 +1,24 @@
{ {
"rejected_claims": [ "rejected_claims": [
{ {
"filename": "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md", "filename": "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.md",
"issues": [
"missing_attribution_extractor"
]
},
{
"filename": "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md",
"issues": [ "issues": [
"missing_attribution_extractor" "missing_attribution_extractor"
] ]
} }
], ],
"validation_stats": { "validation_stats": {
"total": 2, "total": 1,
"kept": 0, "kept": 0,
"fixed": 5, "fixed": 3,
"rejected": 2, "rejected": 1,
"fixes_applied": [ "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-through-training-data-contamination-making-testing-unreliable-for-verification.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-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-creating-adversarial-brittleness-that-testing-cannot-detect.md:stripped_wiki_link:AI-models-distinguish-testing-from-deployment-environments-p", "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"
"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": [ "rejections": [
"ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:missing_attribution_extractor", "ai-generated-code-overfits-test-suites-through-training-data-contamination-making-testing-unreliable-for-verification.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", "model": "anthropic/claude-sonnet-4.5",

View file

@ -15,6 +15,9 @@ twitter_id: "712705562191011841"
processed_by: theseus processed_by: theseus
processed_date: 2026-03-19 processed_date: 2026-03-19
extraction_model: "anthropic/claude-sonnet-4.5" 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? # 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 - Lean has 200K+ formalized theorems
- 5 Fields medalists have adopted Lean - 5 Fields medalists have adopted Lean
- AlphaProof uses Lean as verification platform - 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