Principperne for stærk induktion og deres anvendelse på primtal er grundlæggende for at forstå visse aspekter af talteori. Et vigtigt eksempel på dette er, hvordan vi kan bevise eksistensen af primtalsfaktorer for et givet naturligt tal. Dette gøres ofte gennem induktion, der starter med de simpleste tilfælde og gradvist opbygger et argument for højere værdier. Et interessant princip her er Nat.strong_induction_on, som kan anvendes i beviser, hvor vi ikke nødvendigvis har en base case, da det er dækket af det generelle induktionstrin.
Lad os overveje et eksempel: Antag at vi har et naturligt tal , og vi ønsker at vise, at det enten er et primtal, eller at det har en primfaktor. Antag først, at er et primtal – så er påstanden trivielt sand. Hvis derimod ikke er et primtal, kan vi udnytte definitionen af primtal, som siger, at har en ikke-trivial divisor, . Vi kan derefter anvende induktionshypotesen for at finde en primfaktor for .
Et centralt resultat, der kan anvendes i denne sammenhæng, er følgende sætning: for et naturligt tal , findes der et primtal , der deler . Beviset begynder med at undersøge, om er et primtal. Hvis det ikke er det, opdeles det i faktorer, og vi anvender induktion på disse faktorer for at finde en primfaktor.
Lad os udvide denne tanke til en mere generel påstand om uendeligheden af primtal. Det er velkendt, at der findes et uendeligt antal primtal, og en metode til at bevise dette er at påvise, at for ethvert naturligt tal , findes der et primtal større end . Et klassisk bevis, der anvender faktorialen, viser, at for , der er et naturligt tal, er altid delbart med et primtal, der er større end . Dette indebærer, at der ikke findes en øvre grænse for primtalene, og at de aldrig er begrænsede af et givet tal .
For at formalize dette argument, kan vi bruge den matematiske struktur kaldet Finset i Lean, som repræsenterer endelige mængder af elementer. Når vi arbejder med endelige mængder af primtal, skal vi være opmærksomme på visse særlige egenskaber. For eksempel, hvis et primtal deler et produkt af et sæt primtal, er det nødvendigt at bruge en lemma, der beviser, at nødvendigvis må være et af de primtal, der indgår i sættet.
Et andet nyttigt værktøj er induktion på endelige mængder, Finset.induction_on, som gør det muligt at bevise egenskaber om et vilkårligt element i en endelig mængde. For eksempel kan vi vise, at for enhver endelig mængde af primtal , vil et primtal , der deler produktet af alle elementer i , nødvendigvis være et element i . Dette understøtter påstanden om, at for enhver endelig mængde af primtal, vil der altid være et primtal, der ikke er en del af mængden.
En alternativ formulering af påstanden om, at der findes uendeligt mange primtal, kan være, at for enhver endelig mængde , vil der altid findes et primtal, der ikke tilhører . Dette kan bevises ved at antage, at alle primtal er i , og derefter konstruere en ny mængde , som kun indeholder primtalene i . Produktet af elementerne i , plus én, vil give et tal, der nødvendigvis har en primfaktor, som ikke er i , hvilket fører til en modstrid.
I forbindelse med de ovenstående resultater er det også vigtigt at forstå den algebraiske struktur af mængder og produkter. Når man arbejder med mængder af primtal, skal man være opmærksom på de særlige egenskaber, der gælder for disse mængder, såsom produktet af elementerne i mængden, og hvordan man kan håndtere operationer som unioner og snit mellem mængder.
Det er desuden nødvendigt at tage højde for, at forskellige bevismetoder kan anvendes afhængigt af den valgte logiske tilgang. I nogle tilfælde kan klassisk logik, som giver os mulighed for at antage eksistensen af bestemte egenskaber uden at bekræfte dem direkte, være nyttig. I sådanne tilfælde kan vi bruge teorier som Finset.prod_pos og Finset.dvd_prod_of_mem, som gør det muligt at håndtere uendelige mængder af primtal.
I sidste ende er det klart, at teorier om primtal og deres uendelighed kan formaliseres effektivt ved hjælp af induktion og mængdeteori, især når man arbejder med endelige mængder og deres egenskaber. Denne tilgang åbner dørene til dybere forståelse af talteori og dens forbindelser til andre områder af matematikken.
Er der uendeligt mange primtal kongruente med 3 modulo 4?
Et lille variation af den anden bevismetode, der viser, at der er uendeligt mange primtal, viser, at der også er uendeligt mange primtal, der er kongruente med 3 modulo 4. Argumentet er som følger: Først skal vi bemærke, at hvis produktet af to tal og er kongruent med 3 modulo 4, så må et af de to tal være kongruent med 3 modulo 4. Begge tal skal nemlig være ulige, og hvis de begge er kongruente med 1 modulo 4, så vil deres produkt også være kongruent med 1 modulo 4. Denne observation kan bruges til at vise, at hvis et tal større end 2 er kongruent med 3 modulo 4, så må det tal have en primfaktor, der også er kongruent med 3 modulo 4.
Antag nu, at der kun er et endeligt antal primtal, der er kongruente med 3 modulo 4, lad os sige . Uden tab af generalitet kan vi antage, at . Betragt produktet
Det er let at se, at dette er kongruent med 3 modulo 4, og derfor har det en primfaktor , der er kongruent med 3 modulo 4. Det kan ikke være, at , for hvis var lig med 3, ville også dividere , hvilket ville medføre, at skulle være en af de , for , og vi har allerede ekskluderet 3 fra denne liste. Så må være et af de andre . Men i så fald dividerer , og dermed 3, hvilket er en modstrid, da vi ved, at det ikke kan være lig med 3.
I Lean repræsenterer notationen , der læses "n modulo m", resten af divisionen af med . Eksemplet bekræfter dette. Vi kan dermed udtrykke udsagnet "n er kongruent med 3 modulo 4" som . Et eksempel og nogle teoremer opsummerer de fakta om denne funktion, som vi senere vil bruge. Den første teorem viser et eksempel på ræsonnering gennem et lille antal tilfælde. I den anden teorem, husk at semikolonet betyder, at den efterfølgende taktikblok anvendes på alle mål, der er oprettet af den forudgående taktik.
Når vi taler om et sæt af primtal, skal vi også overveje resultatet af at fjerne 3 fra dette sæt, hvis det er til stede. Funktionen håndterer dette. Et eksempel, der viser dette, kunne være, hvis og er elementer i et finitet sæt , og vi fjerner fra sættet.
Nu er vi klar til at bevise, at der er uendeligt mange primtal kongruente med 3 modulo 4. Hele løsningen bruger Lean’s metoder som og undervejs. Beviset bygger på, at for et vilkårligt , der eksisterer en primfaktor af , der opfylder , hvilket bekræfter, at primtallene kongruente med 3 modulo 4 er uendelige.
I dette bevis anvender vi de grundlæggende regler for division og mod, samt udnytter egenskaberne ved primtalsfaktorisering og modula operationer. Vi benytter os af begreber som induktion og rekursive definitioner for at udføre den nødvendige bevisførelse, hvilket afslører den uendelige natur af primtalene, der er kongruente med 3 modulo 4. Dette er et klassisk resultat i elementær talteori, og den formelle bevisstruktur, der anvendes her, giver en dybere forståelse af, hvordan matematiske ideer som modularitet og primtalinteraktioner spiller sammen.
Som et vigtigt element for læseren er det nødvendigt at forstå, at selvom beviset kan synes komplekst, er det en naturlig forlængelse af grundlæggende talteori. Det er vigtigt at fastholde, at antagelsen om et endeligt antal primtal, der er kongruente med 3 modulo 4, fører til en modstrid, hvilket understøtter påstanden om uendeligheden. Dette resultat har vidtrækkende implikationer for vores forståelse af primtal og deres egenskaber i relation til modulusoperationer. Det er en påmindelse om, at visse teoremer kan kræve dybtgående og præcise teknikker, men den grundlæggende intution bag dem er enkel og kraftfuld.

Deutsch
Francais
Nederlands
Svenska
Norsk
Dansk
Suomi
Espanol
Italiano
Portugues
Magyar
Polski
Cestina
Русский