om stora matematiska modeller fungerar (det verkar som om de kommer att göra det, än så länge), kommer det att vara konstigt att ha en massa tidigare olösta satser bevisade samtidigt som det mycket möjligt inte finns någon människa som kan läsa de modell-Lean-esiska bevisen för att faktiskt veta hur bevisen fungerar

Det fungerar typ så här redan ändå

@_joshd detta kan fungera om sammanfattarmodellen också producerar ett magert bevis som är typidentiskt med originalet