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 nn, og vi ønsker at vise, at det enten er et primtal, eller at det har en primfaktor. Antag først, at nn er et primtal – så er påstanden trivielt sand. Hvis nn derimod ikke er et primtal, kan vi udnytte definitionen af primtal, som siger, at nn har en ikke-trivial divisor, mm. Vi kan derefter anvende induktionshypotesen for at finde en primfaktor for mm.

Et centralt resultat, der kan anvendes i denne sammenhæng, er følgende sætning: for et naturligt tal n2n \geq 2, findes der et primtal pp, der deler nn. Beviset begynder med at undersøge, om nn 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 nn, findes der et primtal større end nn. Et klassisk bevis, der anvender faktorialen, viser, at for nn, der er et naturligt tal, er n!+1n! + 1 altid delbart med et primtal, der er større end nn. Dette indebærer, at der ikke findes en øvre grænse for primtalene, og at de aldrig er begrænsede af et givet tal nn.

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 pp deler et produkt af et sæt primtal, er det nødvendigt at bruge en lemma, der beviser, at pp 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 ss, vil et primtal pp, der deler produktet af alle elementer i ss, nødvendigvis være et element i ss. 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 ss, vil der altid findes et primtal, der ikke tilhører ss. Dette kan bevises ved at antage, at alle primtal er i ss, og derefter konstruere en ny mængde ss', som kun indeholder primtalene i ss. Produktet af elementerne i ss', plus én, vil give et tal, der nødvendigvis har en primfaktor, som ikke er i ss, 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 mm og nn 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 p1,p2,,pkp_1, p_2, \dots, p_k. Uden tab af generalitet kan vi antage, at p1=3p_1 = 3. Betragt produktet

k4i=2kpi+3.k_4 \prod_{i=2}^k p_i + 3.

Det er let at se, at dette er kongruent med 3 modulo 4, og derfor har det en primfaktor pp, der er kongruent med 3 modulo 4. Det kan ikke være, at p=3p = 3, for hvis pp var lig med 3, ville pp også dividere k4i=2kpik_4 \prod_{i=2}^k p_i, hvilket ville medføre, at pp skulle være en af de pip_i, for i=2,,ki = 2, \dots, k, og vi har allerede ekskluderet 3 fra denne liste. Så pp må være et af de andre pip_i. Men i så fald dividerer pp k4i=2kpik_4 \prod_{i=2}^k p_i, og dermed 3, hvilket er en modstrid, da vi ved, at det ikke kan være lig med 3.

I Lean repræsenterer notationen n%mn \% m, der læses "n modulo m", resten af divisionen af nn med mm. Eksemplet 27%4=327 \% 4 = 3 bekræfter dette. Vi kan dermed udtrykke udsagnet "n er kongruent med 3 modulo 4" som n%4=3n \% 4 = 3. 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 Finset.eraseFinset.erase håndterer dette. Et eksempel, der viser dette, kunne være, hvis mm og nn er elementer i et finitet sæt ss, og vi fjerner nn 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 Nat.dvdaddiffleftNat.dvd_add_iff_left og Nat.dvdsubNat.dvd_sub' undervejs. Beviset bygger på, at for et vilkårligt nn, der eksisterer en primfaktor pp af k4i=2kpi+3k_4 \prod_{i=2}^k p_i + 3, der opfylder p%4=3p \% 4 = 3, 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.