Quando o Código Vira Commodity: O Trunfo do Matemático

Em fevereiro de 2026, um advogado venceu o Hackathon da Anthropic, e um cardiologista ficou em terceiro com uma plataforma de IA na área médica. Treze mil candidatos competiram; nenhum dos vencedores escreveu código. Além disso, o Bureau de Estatísticas do Trabalho dos EUA reporta uma queda de 27,5% nas vagas de programador entre 2023 e 2025, enquanto a Levels.fyi afirma que a nova especialidade “AI Engineer” está pagando um prêmio salarial de 18,7% sobre o staff e foi eleita pelo LinkedIn como a função que mais cresce pelo segundo ano seguido.

Nesse contexto, vem a provocação: se código está virando commodity, o que é escasso?

Este artigo trabalha com três fontes de evidência: benchmarks de IA em matemática, dados do mercado de trabalho dos EUA na área de engenharia, e um artigo de 2026 de Klowden e Tao sobre a estrutura de trabalho dos humanos ao lado da IA. Os números refletem um retrato de abril de 2026. O argumento é estrutural, não preditivo: a fronteira onde a IA para de funcionar tem um formato, e esse formato recompensa um tipo específico de julgamento humano.

Baseado em palestra ministrada no Departamento de Matemática da UFSC em 24 de abril de 2026 para alunos de doutorado e mestrado em matemática. Slides: English (PDF) · Português (PDF).

Termos-chave

• IMO (International Mathematical Olympiad): competição anual de ensino médio; referência para raciocínio matemático.
• USAMO (USA Mathematical Olympiad): qualificatória nacional dos EUA para a IMO; problemas de demonstração matemática corrigidos por juízes humanos.
• FrontierMath Tier 4 (benchmark da Epoch AI): problemas matemáticos de nível de pesquisa, projetados para permanecer não-saturados pelos modelos atuais.
• Lean 4 / Mathlib: uma linguagem de demonstração formal e sua biblioteca central; o Mathlib carrega cerca de 1,9 milhão de linhas de matemática verificada, mantida por mais de 500 contribuidores.
• Smell test (Klowden & Tao §4.2): a heurística que matemáticos aplicam antes de ler uma demonstração linha a linha, usada para detectar argumentos ruins cedo.
• Demonstração sem cheiro (K&T §4.6 n16): um resultado formalmente correto que não tem a narrativa causal que os humanos usam para julgar trabalho matemático.
• Blue team / red team (K&T §6.2): papéis de geração versus verificação, emprestados da cibersegurança. K&T argumentam que a IA é relativamente segura no red team, insegura no blue.
• Software 3.0 (Karpathy, junho de 2025): software produzido por descrição em linguagem natural, distinto do código que humanos escrevem (1.0) ou de modelos que humanos treinam (2.0).

Por que desta vez é diferente

Automações anteriores afetaram a periferia do trabalho intelectual: a prensa de Gutenberg, a máquina de escrever, o LaTeX e a internet. Todas elas mudaram como ideias eram copiadas, transmitidas e renderizadas. O trabalho de gerar ideias, de decidir o que escrever, continuou humano. Klowden e Tao abrem o seu artigo de 2026 com essa distinção: a IA moderna é a primeira tecnologia de propósito geral que automatiza o processo de criação em si, não apenas a etapa de disseminação.

O ponto importa para o que se segue neste artigo. Se uma ferramenta automatiza apenas a disseminação, a pergunta “o que é escasso” segue trivialmente respondida: a produção de novas ideias. Quando a ferramenta começa a produzir resultados que parecem ideias (demonstrações, rascunhos, código, diagramas), a pergunta vira estrutural. Mera retórica não vai responder. A resposta honesta começa onde a ferramenta falha.

Critério e dificuldade: o gap tem duas fontes

Em abril de 2026, os melhores modelos saturam acima de 99% na matemática de competição quando só a resposta final é avaliada. Perdem terreno em dois eixos: quando o critério passa a exigir demonstração matemática completa avaliada por humanos, e quando a dificuldade sobe ao nível de pesquisa.

O que a tabela mostra: dois fatores derrubam os scores ao mesmo tempo.

No mesmo conjunto de problemas, basta mudar o critério, de “resposta final correta” para “demonstração completa correta”, e o score cai. Sobre os mesmos 5.062 problemas, o Open Proof Corpus mediu quedas de 8 pontos percentuais (Gemini-2.5-Pro) a 30 pontos (o3), dependendo do modelo.

Mantido o critério de resposta final, a dificuldade pesa ainda mais. AIME 2025 (qualificatória olímpica) supera 99%; FrontierMath Tier 4, com o mesmo critério mas problemas de nível de pesquisa, fica em ~38%. São cerca de 60 pontos percentuais vindos só da subida de dificuldade.

Cruzando os dois eixos, Open Proof Corpus chega a 43% (problemas olímpicos com demonstração avaliada por humanos) e FormalProofBench a 33,5% (problemas de pós-graduação com demonstração formal em Lean).

A diferença não é ruído de medição. Acompanha duas fronteiras ao mesmo tempo: o critério (resposta certa vs demonstração verificável) e a dificuldade (problema solucionável vs problema de pesquisa). O resto do artigo se organiza em torno desses dois eixos.

A IMO 2025 é o cruzamento mais visível dos dois eixos: dificuldade no topo da olimpíada pré-universitária e demonstração corrigida pelos juízes oficiais lendo o argumento inteiro. O que chama atenção é que, mesmo nessa combinação, os 35/42 ≈ 83% do Gemini Deep Think e do modelo experimental da OpenAI ficam em nível de medalha de ouro, e o salto até esse patamar foi rápido. Em 2024, o AlphaProof da DeepMind levou 28/42 (medalha de prata) com demonstrações formais em Lean 4 e vários dias de computação por problema. Em 2025, Gemini Deep Think chegou a 35/42 em linguagem natural dentro da janela de 4,5 horas da prova, certificado pelos coordenadores da IMO. Doze meses depois, o que exigia Lean formal e dias de computação coube em linguagem natural dentro da janela da prova. Mesmo com isso, o problema 6 ficou sem solução, e o gap em relação aos 99,8% do AIME mantém o critério como fronteira viva.

Os benchmarks de resposta final em nível olímpico (MATH-500, AIME 2025, GSM-8K) já não diferenciam os modelos líderes. Há poucos anos, estavam confortavelmente fora de alcance. Hoje, são piso.

As notícias do avanço das IAs são ecoadas aos trombones. Mas sob a perspectiva da demonstração correta e dos problemas de pesquisa, ainda estamos ao som de violinos. O trabalho interessante começa abaixo do abismo.

Do que o abismo é feito

Os números da seção anterior dizem que o abismo existe; não dizem como ele se forma. A literatura recente sobre falhas de raciocínio em modelos de fronteira aponta para três modos recorrentes:

• Um único passo alucinado invalida uma cadeia inteira de derivação.
• A memória de trabalho colapsa em torno de 20 a 30 ramos paralelos, independentemente da escala do modelo; o teto não se move com a contagem de parâmetros.
• O grupo de pesquisa da Apple documentou “colapso completo de acurácia além de certas complexidades” em 2025: o esforço de raciocínio cresce por um tempo, depois cai, como se o sistema desistisse.

Klowden e Tao nomeiam a versão mais profunda dessa falha de “demonstrações sem cheiro”. As soluções do AlphaProof na IMO 2024 foram verificadas como corretas pelo Lean. Continham também passos redundantes e saltos inexplicáveis. As demonstrações estavam formalmente certas sem estar legivelmente coerentes: faltava a elas o que Thurston (1994/2006) identificou como a marca da boa matemática, uma narrativa causal que permite ao leitor ver por que a conclusão segue, não apenas que segue. O sistema passa pelo verificador e falha no smell test que o matemático aplicaria antes de abrir o Lean.

Essa distinção monta o resto do argumento. O mercado de trabalho está registrando a mesma fronteira por outro ângulo.

Os dados de trabalho, lidos junto com o abismo

Antes de seguir, uma ressalva. A leitura do mercado de desenvolvimento de software vem de oito anos do autor na indústria, entre consultoria em machine learning e finanças quantitativas. O material matemático fica em terreno mais familiar do que os dados empíricos do mercado de trabalho, e os casos corporativos citados abaixo refletem o que o autor viu de perto, não uma amostra estatística.

O registro empírico sobre desenvolvimento de software júnior já é denso.

O que isso mostra: bifurcação, não extinção. O papel de programador focado em execução está encolhendo; o papel orientado a design que colabora com IA está se expandindo. São dois trabalhos diferentes que por acaso compartilham um rótulo histórico.

A sinalização corporativa se alinha com os dados, embora o sinal venha misturado com narrativa. A Salesforce anunciou zero novas contratações de engenheiros para o ano fiscal de 2026. A Shopify acrescentou uma política exigindo justificativa por escrito de que a IA não consegue fazer o trabalho antes que qualquer nova vaga possa ser aprovada. A Microsoft atribuiu cerca de 6.000 demissões em maio de 2025 em parte à produtividade interna de IA, citando que 20 a 30% do código novo está sendo escrito por IA. A Amazon anunciou 14.000 cortes corporativos em outubro de 2025 com IA citada.

Mas há, na verdade, pouco suporte estatístico para uma afirmação conclusiva. O Federal Reserve dos EUA, em estudo de março de 2026 cobrindo mais de um milhão de empresas, não encontrou ligação estatisticamente significativa entre adoção de IA e contratação agregada. A Klarna, caso de manchete para redução de força de trabalho via IA, cortou de cerca de 5.500 para 3.000 empregados enquanto adotava IA, viu a receita por funcionário multiplicar cerca de quatro vezes (de US$300 mil para US$1,3 milhão) e depois reverteu parcialmente em maio de 2025, recontratando humanos depois que a qualidade do trabalho de atendimento ao cliente caiu (zero surpresas). Inclusive, o próprio BLS projeta crescimento agregado de +15% no setor até 2034.

Onde a IA efetivamente pode substituir um humano e quanto da mudança recente pode ser atribuído a ela especificamente são perguntas em aberto que a evidência e o tempo ainda não esclareceram.

Uma observação pessoal. Uma tesouraria que o autor antes gerenciava e desenvolvia com dois ou três colegas hoje cabe em uma pessoa só, com IA. Num contexto recente, ele atua como cientista de risco solo, acumulando o papel de engenheiro principal do projeto. É o tipo de percepção que a evidência macro terá de confirmar ou descartar. O relato aponta numa direção clara: a capacidade de engenharia, que era o principal gargalo, virou commodity.

Para onde o gargalo se moveu

A McKinsey, em seu State of AI 2025, constata que apenas 39% das empresas que adotaram IA generativa relatam impacto mensurável de EBIT (lucro antes de juros e impostos). O instituto da IBM relata que um em cada quatro projetos de IA entrega o retorno prometido. O ensaio de junho de 2025 da Faktion diagnostica o modo de falha recorrente: “o conhecimento está espalhado pela documentação, sistemas legados e, mais criticamente, na cabeça de uns poucos especialistas calejados”. Boris Cherny, responsável pelo Claude Code na Anthropic, no Lenny’s Podcast em fevereiro de 2026: “o problema central agora é saber o que diabos você de fato quer construir”.

Ambos sinais convergem para o mesmo lugar: quando engenharia deixa de ser o gargalo, sobra o trabalho de saber o que construir - papel desempenhado principalmente por especialistas da área.

A restrição se deslocou de capacidade de engenharia para enquadramento de problemas, expertise de domínio e a habilidade de definir critérios claros de sucesso num cenário que a IA não consegue inferir. Cinco nichos na área de matemática tornam essa fronteira concreta (recorte qualitativo, baseado no que o autor observa):

• Pesquisa em alinhamento na Anthropic e no programa MATS, com vagas em análise de reward hacking e dinâmicas de treinamento.
• Verificação formal: especialistas, US$70-150 por hora pela Alignerr, exigindo fluência em Lean 4 e Mathlib.
• Teoria de ML: um campo enxuto com forte apetite por trabalho de interpretabilidade e generalização, em que a ausência de um arcabouço matemático estabelecido é em si a oportunidade.
• Finanças quantitativas: modelagem estocástica combinada com machine learning, demanda sustentada por quants que dominem ambos.
• Pesquisa operacional: o trabalho de formular problemas. Definir variáveis, restrições e a função objetivo. Esse passo de formulação é exatamente o que a IA não consegue fazer sem um humano que saiba o que está sendo otimizado.

São domínios onde rigor e demonstração não podem ser automatizados, e onde a IA amplifica o matemático sem substituir o julgamento do matemático. A bifurcação no mercado de trabalho e o abismo nos benchmarks apontam para a mesma lacuna.

O smell test, formalizado

Os matemáticos têm um nome para a habilidade que falta, ainda que não apareça em nenhum slide de laboratório de IA. O post de blog de 2008 de Scott Aaronson, Ten Signs a Claimed Mathematical Breakthrough is Wrong, lista dez heurísticas que matemáticos experientes aplicam, com frequência subconscientemente, para detectar argumentos ruins bem antes da verificação linha a linha:

1. Os autores não usam TeX.
2. Os autores não entendem a pergunta.
3. A abordagem implica algo muito mais forte e provavelmente falso.
4. A abordagem contradiz um resultado de impossibilidade conhecido.
5. Os autores trocam silenciosamente “demonstramos” por “parece funcionar em todos os casos que tentamos” no meio do caminho.
6. O artigo pula para tecnicalidades sem uma ideia nova.
7. O artigo não se baseia em trabalho prévio.
8. O artigo gasta tempo definindo termos padrão.
9. O artigo se aprofunda poeticamente sobre “consequências práticas”, “profundas implicações filosóficas”, etc.
10. As técnicas parecem fracas demais para o problema.

Klowden e Tao §4.2 chamam isso de “smell test” e argumentam que é o aspecto da prática matemática que mais resiste às arquiteturas atuais de IA. LLMs (modelos de linguagem de grande porte) são treinados para produzir saídas que parecem corretas, que é exatamente o modo de falha que o smell test foi construído para detectar. Vários dos sinais de Aaronson (as palavras evasivas no #5, as tecnicalidades sem ideia no #6, a retórica sobre implicações no #9) são padrões que os modelos atuais exibem por construção. Detectá-los exige três coisas:

• Familiaridade profunda com trabalho prévio.
• Intuição sobre que tipos de afirmação tendem a ser verdadeiros.
• Sensibilidade à forma como matemáticos reagem a uma afirmação nova.

Nenhuma dessas é produzida de forma confiável pelas LLMs atuais. Isso explica a localização do abismo. O abismo não é arbitrário, ele acompanha a fronteira entre problemas onde o smell test é desnecessário (aritmética de resposta final no nível AIME) e problemas onde o smell test é a habilidade que sustenta o trabalho (verificação de demonstração em nível de pesquisa, avaliação de afirmação nova, parecer de artigo). Aumentar capacidade bruta dos modelos não fechou essa fronteira, porque a arquitetura atual não foi desenhada para resolvê-la.

O kit de ferramentas atual

A fronteira de “IA na pesquisa em matemática” é concreta, não hipotética. Novembro de 2025: Terence Tao publicou um relato descrevendo um ano de colaboração com a Google DeepMind. AlphaEvolve mais Gemini Deep Think foram aplicados a 67 problemas matemáticos em aberto em combinatória, análise e teoria dos números, produzindo cerca de 20 resultados genuinamente novos, com um subconjunto de demonstrações passando na verificação formal em Lean 4. O fluxo de trabalho adotado foi o seguinte:

flowchart LR
    A[AlphaEvolve
descobre candidato] --> B[Deep Think
esboça demonstração]
    B --> C[AlphaProof
formaliza em Lean]
    C --> D[Lean 4
verificado]

Tao seleciona e avalia os problemas no início do loop e julga o insight resultante no fim.

O mesmo padrão em escala mais acessível: em agosto de 2025, Ernest Ryu (Seoul National University, antes UCLA) usou GPT-5 como assistente e melhorou em cerca de 50% o melhor limite conhecido em um problema de operator splitting e métodos de primeira ordem em otimização convexa, em aberto há 40 anos. O resultado foi publicado como nota rigorosa, não apenas heurística.

Mesmo padrão: o humano escolhe o problema e julga o insight; a máquina trabalha nas etapas intermediárias.

A infraestrutura é aberta e documentada. Lean 4 com Mathlib carrega cerca de 1,9 milhão de linhas de matemática formalmente verificada. O LeanCopilot, da Caltech, sugere táticas Lean durante demonstrações. O DeepSeek-Prover-V2 decompõe problemas em outros menores (dividir para conquistar). Kimina-Prover, da Moonshot, foi o primeiro provador a passar de 80% no MiniF2F. Nada disso exige acesso especial.

Os sistemas com acesso restrito estendem o teto: AlphaProof, AlphaEvolve e o preview do Claude Mythos no Project Glasswing da Anthropic (que reportou 97,6% no USAMO 2026, sem correção independente publicada). Ainda assim, as ferramentas públicas já funcionam como bons assistentes para o matemático em trabalho em nível de pesquisa.

Um segundo ponto convém mencionar, sobretudo para quem não escreve código. O enquadramento de Andrej Karpathy “Software 3.0”, de junho de 2025, nomeia um novo modo: programas que humanos descrevem em linguagem natural.

• Software 1.0: código que humanos escrevem.
• Software 2.0: modelos que humanos treinam.
• Software 3.0: software produzido por descrição em linguagem natural.

Trent Field, que não escreve código profissionalmente, trabalha na Arkance e apresentou na Autodesk University 2025 uma aplicação web funcional que construiu sozinho em 48 horas usando Cursor. O advogado, o cardiologista e os matemáticos que provam novos resultados em colaboração com IA não são exceções; marcam o mesmo padrão: a IA atravessou da disseminação para a criação. O arranjo só funciona enquanto o humano consegue verificar o que a IA produz.

A regra operacional

Klowden e Tao §6.2 propõem uma regra com vocabulário emprestado da cibersegurança. A IA é relativamente segura para usar como red team (revisando conteúdo gerado por humanos em busca de erros ou sugerindo melhorias) e insegura para confiar como blue team (gerando conteúdo estrutural além do que um red team pode verificar). O red team pode ser revisores humanos, assistentes de demonstração formal como Lean, ou outros sistemas de IA rodando em capacidade de verificação. O que o blue team produz precisa ficar dentro do que o red team consegue checar.

A regra é fácil de enunciar e fácil de violar. Enquanto rascunhava a palestra que originou este artigo, o autor pediu a uma IA para escrever um slide explicando o enquadramento de K&T. Ela produziu “a IA é potente no blue team, o red team é função humana”, o que mistura os conceitos da tese de K&T. O autor notou a confusão na primeira leitura. Duas rodadas adicionais de feedback à IA falharam em trazer isso à tona; o slide errado continuava voltando. A tese de K&T se demonstrou: o smell test é a camada que nenhum modelo atual tem de forma confiável, e foi o que produziu o parágrafo corrigido.

Uma segunda instância do mesmo efeito apareceu depois da palestra. Um aluno de pós-graduação que assistiu apontou que os slides usavam em-dashes (travessões) liberalmente, um indicativo de conteúdo gerado por IA. Ele não estava checando a matemática. Estava aplicando o smell test ao meio e lendo a assinatura na superfície.

A regra operacional, então, em duas frases:

1. Deixe a IA verificar o seu trabalho, não gerar trabalho que você não consegue verificar.

2. Ao verificar o trabalho da IA, aplique seu faro matemático para invalidar argumentos; esse faro o modelo não tem.

Limitações

Os scores dos benchmarks neste texto são um retrato até 18 de abril de 2026 (GPT-5.5, lançado em 23 de abril, e DeepSeek V4, em preview desde 24 de abril, ficam fora dessa análise). Dito isto, é importante reconhecer que tais números rapidamente ficam desatualizados; espere que os números específicos estejam desatualizados em semanas. A própria caracterização pública de Tao sobre IA para pesquisa mudou ao longo de dezoito meses:

O ritmo não está desacelerando. O lançamento do GPT-5.4 para o GPT-5.5, por exemplo, levou cerca de sete semanas (de 5 de março a 23 de abril de 2026), e o FrontierMath Tier 4 saltou de 38% para 39,6% (GPT-5.5 Pro) nesse intervalo.

Os dados de trabalho apresentados neste texto estão fortemente concentrados nos EUA. O resultado nulo do Federal Reserve e a reversão da Klarna mostram heterogeneidade real em como a adoção de IA se traduz em mudanças nos recursos humanos. O enquadramento do trunfo matemático presume que o smell test continue fora de alcance para as arquiteturas atuais. Essa é uma afirmação sobre como os modelos de hoje são treinados, não uma previsão sobre o que um modelo futuro poderá fazer. Se a arquitetura mudar, o argumento estrutural precisa ser reconsiderado.

Uma ressalva final. Os casos de sinalização corporativa (Salesforce, Shopify, Microsoft, Amazon) carregam peso narrativo e incentivos financeiros além de intenção de contratação. Declarações públicas de CEOs são escritas para investidores em primeiro lugar; se refletem realidade operacional é uma questão à parte. As duas lacunas recorrentes (quando não abismos) são:

1. Afirmações deliberadamente erradas;
2. Enquadramento seletivo.

Em geral, ambos servem para surfar uma narrativa do momento. O enquadramento seletivo, em particular, aparece em ganhos de eficiência atribuídos à IA quando outros programas de custo foram o motor maior, ou em mudanças nos recursos humanos atribuídas à automação quando os cortes já estavam previstos independentemente da IA.

Leia nas entrelinhas. O fluxo de caixa dessas empresas é mais informativo que as declarações de seus CEOs, como Michael Burry demonstra em seu blog Cassandra Unchained.

Síntese

O abismo de capacidade e a bifurcação no mercado de trabalho apontam para a mesma coisa. Onde o trabalho é verificável de ponta a ponta (benchmarks de resposta final, tarefas de engenharia com escopo bem definido), a IA commoditizou a oferta. Onde a verificação depende do smell test (demonstrações em nível de pesquisa, afirmações novas, enquadramento de problemas), o papel humano é estrutural: o recurso escasso que ninguém commoditizou.

A regra operacional é curta: deixe a IA verificar o seu trabalho, e não a deixe gerar trabalho que você não consegue verificar. A habilidade por trás dessa regra é o smell test, o faro do matemático, treinado em anos de conteúdo matemático real. Essa é a parte que tanto os dados de trabalho quanto os benchmarks insistem em revelar como escassa.

Leitura complementar

Slides da palestra

• When Code Becomes a Commodity: The Mathematician’s Edge — English (PDF) — UFSC Mathematics Department, 24 April 2026
• Quando o Código Vira Commodity: o Trunfo do Matemático — Português (PDF) — Departamento de Matemática da UFSC, 24 de abril de 2026

Fontes primárias

• Klowden, T. & Tao, T. Mathematical Methods and Human Thought in the Age of AI (arXiv:2603.26524, March 2026)
• Aaronson, S. Ten Signs a Claimed Mathematical Breakthrough is Wrong (Shtetl-Optimized, January 2008)
• Thurston, W. P. On Proof and Progress in Mathematics (arXiv:math/9404236, 1994; reprinted in 18 Unconventional Essays on the Nature of Mathematics, R. Hersh, ed., Springer, 2006)
• Tao, T. Mathematical exploration and discovery at scale (personal blog, 5 November 2025)
• Tao, T. AI is ready for primetime (OpenAI Academy at IPAM, 6 March 2026)
• Tao, T. Mastodon post on AI mathematical capability (@tao on mathstodon.xyz, September 2024)

Capability benchmarks (math)

• De Koninck et al. Open Proof Corpus (arXiv:2506.21621, ETH Zurich, June 2025)
• FormalProofBench (arXiv:2603.26996, March 2026)
• Apple Machine Learning Research. The Illusion of Thinking (2025)
• Self-consistency hallucination detection in LLM reasoning chains (arXiv:2504.09440)
• Diagnosing algebraic reasoning failures: 20-30 parallel-branch ceiling (arXiv:2604.06799)
• DeepMind. AI achieves silver-medal standard at the IMO (2024)
• DeepMind. Gemini Deep Think achieves gold-medal standard at the IMO (2025)
• Epoch AI. FrontierMath benchmark
• DeepMind. AlphaGeometry 2 (arXiv:2502.03544)
• Diez, da Maia, Nourdin. Mathematical research with GPT-5 (arXiv:2509.03065)
• Axiom Math. AxiomProver / Putnam 2025
• Anthropic. Claude Mythos Preview System Card and Project Glasswing
• MATH-500 leaderboard

Labor and economic data

• Brynjolfsson, Chandar & Chen. Canaries in the Coal Mine? Six Facts About the Recent Employment Effects of AI (Stanford Digital Economy Lab, 13 November 2025)
• Hosseini Maasoum & Lichtinger. Generative AI as Seniority-Biased Technological Change (SSRN 5425555, 31 August 2025)
• Westby & Sasser Modestino. The Impact of Generative AI on Job Opportunities for Junior Software Developers (Northeastern, 16 June 2025)
• LeadDev. AI Impact Report 2025 (54% of engineering leaders expect fewer junior hires) — PDF
• US BLS Occupational Employment Statistics: Programmers (15-1251) and Software Developers (15-1252)
• US BLS Occupational Outlook Handbook: Software Developers (+15% through 2034)
• Federal Reserve Bank of New York. The Labor Market for Recent College Graduates (CS graduate unemployment data)
• The Register. UK tech grad hiring crashes 46% as bots do junior work (October 2025; reporting on Institute of Student Employers data)
• Levels.fyi AI Engineer Compensation Trends Q3 2025
• LinkedIn News. Jobs on the Rise 2025
• Stack Overflow. Developer Survey 2025 (84% of developers using or planning to use AI coding tools)
• GeekWire. AI-native startup survey (late 2025) (68% of AI-native startups have AI writing >80% of production code)

Industry signal

• McKinsey. State of AI 2025 (39% of enterprises report measurable EBIT impact)
• IBM Institute for Business Value. CEOs Double Down on AI While Navigating Enterprise Hurdles (May 2025; 2,000 CEOs across 33 countries; 25% of AI initiatives delivered expected ROI)
• Michael Burry. Cassandra Unchained (Substack; cash-flow-driven reading of corporate AI claims)
• Vanalphen / Faktion. Smart Isn’t Enough: Why AI Needs to Understand Like a Human Expert (June 2025)
• Lenny’s Podcast. Head of Claude Code: What happens after coding is solved (Boris Cherny, Feb 2026)
• Fortune. As Klarna flips from AI-first to hiring people again (May 2025)
• Fortune. Prompt engineer title falls off the map (May 2025) (citing Indeed Hiring Lab)
• Federal Reserve. Monitoring AI Adoption in the US Economy (March 2026; null result on AI adoption vs. hiring)
• Tech.co. Companies That Have Replaced Workers with AI in 2025 and 2026 (Salesforce zero hires)
• CNBC. Shopify CEO: Prove AI can’t do jobs before asking for more headcount (April 2025)
• TechCrunch. Microsoft CEO says up to 30% of the company’s code was written by AI (April 2025; context for May 2025 layoffs)
• Computer Weekly. Amazon links planned mass layoff to AI (October 2025)
• OpenAI. Harness Engineering (>1M lines of code with zero human authors)
• India Today. Cardiologist builds AI health platform in 7 days, wins 3rd prize at hackathon (Feb 2026)

Tools and toolkit

• Karpathy, A. Software 3.0 (AI Startup School keynote, 17 June 2025)
• OpenAI. GPT-5 mathematical discovery (Ryu convex-optimization improvement, August 2025)
• Lean 4 official site — language and toolchain
• Mathlib (leanprover-community) and Mathlib stats (1.9M lines, 500+ contributors)
• AlphaProof — olympiad-level formal reasoning (Nature) (peer-reviewed write-up of the IMO-2024 silver result)
• Moonshot AI. Kimina-Prover-Preview (>80% MiniF2F)
• Wolfram. Foundation Tool (callable from Claude / GPT)
• Field, T. & Beale. Vibe Coding for the Fearless (Autodesk University 2025) and APS Blog companion post
• Anthropic pricing, OpenAI pricing, Google AI Ultra subscriptions
• CFA Institute. AI Top of Mind in 2024 Asset Manager Survey (64% of investment professionals upskilling on AI/ML)