Each language version is independently generated for its own context, not a direct translation.
Stel je voor dat je een heel ingewikkeld raadsel oplost, zoals een Sudoku of een ontsnappingsspel. Je hebt twee manieren om dit te doen:
- De "Snelle, Chaotische" Manier (Apply-Style): Je probeert van alles. "Als ik hier deze knop druk, gebeurt dat dan? Nee? Oké, dan die andere." Je schrijft een lijstje met instructies op: "Druk op A, druk op B, druk op C." Het werkt snel om het antwoord te vinden, maar als je de lijstje een week later terugkijkt, vraag je je af: "Waarom deed ik dat? Wat was het doel van stap 3?" Als één knopje verandert (bijvoorbeeld omdat de regels van het spel zijn aangepast), breekt je hele lijstje en weet je niet meer waar het misging.
- De "Duidelijke, Logische" Manier (Isar): Je schrijft een verhaal op. "Eerst bewijzen we X. Omdat X waar is, weten we dat Y ook waar is. En omdat Y waar is, is Z het antwoord." Dit is langzamer om te schrijven, maar het is superleesbaar. Als de regels veranderen, zie je direct waar het verhaal hakt en kun je het makkelijk repareren.
Het probleem: Veel mensen in de wereld van wiskundige bewijzen (met een computerprogramma genaamd Isabelle) houden van de snelle, chaotische manier om snel een oplossing te vinden. Maar ze weten dat de duidelijke manier beter is voor de lange termijn. Het probleem is dat het overschakelen van de ene naar de andere manier heel veel handwerk kost. Je moet je lijstje met knopjes één voor één omzetten in een verhaal.
De oplossing: Apply2Isar
De auteurs van dit paper hebben een slimme robot genaamd Apply2Isar gebouwd. Dit is een tool die automatisch jouw "snelle lijstje" omzet in een "duidelijk verhaal".
Hier is hoe het werkt, met een paar creatieve vergelijkingen:
De Reisverslag-Vertaler:
Stel je voor dat je een reis hebt gemaakt en alleen maar een lijstje met coördinaten hebt opgeschreven: "Ga 100m noord, draai rechts, ga 50m." Dat is de Apply-Style.
Apply2Isar neemt die lijst, loopt de route virtueel opnieuw af, en schrijft een mooi reisverslag: "We begonnen in het dorp. We liepen naar de berg, waar we een mooi uitzicht zagen. Vervolgens daalden we af naar de rivier." Dat is de Isar-Style.
Het mooie is: de robot onthoudt precies wat er op elk moment gebeurde, zodat het verhaal klopt.De "Tijdbesparende" Vertaler:
Zonder deze tool zou een mens uren moeten besteden aan het vertalen van een bewijs. Met Apply2Isar duurt het seconden. Je kunt je "ruwe" bewijs schrijven, en de tool maakt er direct een "gladde" versie van.Het "Reparatie-Werk" (Robuustheid):
Stel je voor dat je een huis bouwt met een losse stenen muur (Apply-Style). Als je één steen verwijdert, kan de hele muur instorten en weet je niet welke steen het probleem was.
Met Apply2Isar bouw je het huis van bakstenen met cement (Isar). Als je één steen verwijdert, zie je direct dat die specifieke muur instort, maar de rest van het huis blijft staan. Het is veel makkelijker om te repareren.
Hoe goed werkt het?
De auteurs hebben de tool getest op duizenden bestaande bewijzen uit een grote bibliotheek (de Archive of Formal Proofs).
- Resultaat: In 95% tot 99% van de gevallen slaagde de tool erin om het bewijs volledig of grotendeels om te zetten.
- De "Gevallen" (Uitzonderingen): Soms zijn de bewijzen zo raar of gebruiken ze speciale symbolen die de robot even niet begrijpt. Dan stopt de robot en zegt: "Ik heb dit gedeelte vertaald, maar dit stukje moet je zelf nog even doen." Dit noemen ze een "gedeeltelijke vertaling".
Waarom is dit belangrijk?
Vroeger moesten mensen kiezen tussen "snel werken" en "duidelijk werken". Met Apply2Isar kun je het beste van beide werelden hebben:
- Je werkt snel en experimenteert met je bewijs (zoals een wetenschapper in een lab).
- Zodra je het hebt, klik je op een knop en krijg je een prachtig, leesbaar en veilig bewijs dat iedereen kan begrijpen en makkelijk kan onderhouden.
Kortom: Apply2Isar is de tolk die jouw snelle, cryptische notities omzet in een prachtig verhaal dat iedereen kan lezen.