Perché esistono infiniti numeri primi congruenti a 3 modulo 4?

Una variazione sottile ma significativa della seconda dimostrazione classica dell’infinità dei numeri primi mostra che esistono infiniti numeri primi congruenti a 3 modulo 4. L’argomento si basa su una proprietà fondamentale dei residui quadratici: se il prodotto di due numeri $m$ e $n$ è congruente a 3 modulo 4, allora almeno uno dei due numeri deve essere congruente a 3 modulo 4. Questo si spiega osservando che entrambi i numeri devono essere dispari, e se entrambi fossero congruenti a 1 modulo 4, anche il loro prodotto lo sarebbe, escludendo quindi il caso modulo 3.

Per formalizzare rigorosamente questo ragionamento, si introduce la notazione $n \% m$ per indicare il resto della divisione di $n$ per $m$, così che la congruenza modulo 4 diventa $n \% 4 = 3$. Alcuni teoremi fondamentali sono necessari: per esempio, che se $m \cdot n \equiv 3 \pmod{4}$, allora $m \equiv 3 \pmod{4}$ o $n \equiv 3 \pmod{4}$, e che ogni numero congruente a 3 modulo 4 è almeno 2.

Per completare la dimostrazione dell’infinità dei primi congruenti a 3 modulo 4, si considera un insieme finito $s$ di tali primi e si costruisce un nuovo numero congruente a 3 modulo 4 che deve avere un fattore primo non appartenente a $s$, ottenendo un’altra contraddizione.

È essenziale comprendere che la tecnica di costruzione di numeri con determinate proprietà modulari e l’analisi dei loro fattori primi non solo servono per dimostrare l’infinità di una classe di primi, ma aprono la strada a studi più profondi, come quelli sui numeri primi in progressioni aritmetiche e sui residui quadratici. Inoltre, la formalizzazione di questi risultati in linguaggi di prova assistita, come Lean, sottolinea l’importanza di un rigore formale crescente nella matematica moderna, che può prevenire ambiguità e assicurare la validità delle dimostrazioni.

Un altro aspetto importante è l’uso di strumenti di induzione ben strutturati per affrontare definizioni ricorsive e dimostrazioni di proprietà complesse di funzioni aritmetiche, come nel caso della funzione fattoriale o della successione di Fibonacci. Questi metodi inducono a una comprensione più profonda delle relazioni tra definizioni ricorsive e prove per induzione, mostrando come tali tecniche siano fondamentali non solo in teoria dei numeri ma anche in altre branche della matematica.

Per il lettore è utile tenere presente come questi concetti si inseriscano in un quadro più ampio: la teoria dei numeri moderna si avvale spesso di combinazioni di metodi analitici, algebrici e computazionali. Le dimostrazioni di infinità dei primi con certe proprietà modulari sono tappe fondamentali per studiare teoremi più complessi, come quelli relativi alla distribuzione dei primi e alla loro densità in progressioni aritmetiche. Infine, la formalizzazione automatizzata delle dimostrazioni rappresenta un’innovazione che non solo migliora la certezza matematica, ma anche la possibilità di esplorare problemi altrimenti inaccessibili tramite calcolo umano diretto.

Cosa sono i monoidi, i gruppi e i sottogruppi nella formalizzazione matematica?

L'importanza dei monoidi non è tanto nella loro frequente manipolazione diretta durante le dimostrazioni, quanto nel fatto che molte altre strutture — come i gruppi, gli anelli e persino strutture più complesse — sono costruite su di essi. Per esempio, i numeri naturali con l'addizione formano un monoid, ma non un gruppo, poiché non tutti gli elementi hanno un inverso. Questo rende il concetto di monoid più adatto in contesti dove non è necessario postulare l'invertibilità.

In Mathlib, i monoidi sono rappresentati dalla classe di tipo Monoid M, che utilizza notazione moltiplicativa per default. Se si preferisce la notazione additiva, si usa AddMonoid. Le versioni commutative si ottengono semplicemente anteponendo Comm. Questo sistema flessibile permette una tipizzazione coerente con i comportamenti attesi delle strutture, mantenendo la possibilità di interscambiare notazioni secondo il contesto.

Una volta definito un monoid, è possibile considerare le morfismi di monoidi, ovvero applicazioni che preservano la struttura. Tali morfismi sono rappresentati come MonoidHom M N, e vengono automaticamente trattati come funzioni da $M$ a $N$ quando applicate ad elementi. Anche qui, esistono versioni additive AddMonoidHom, scritte con la freccia $\rightarrow^+$. In entrambi i casi, le proprietà come la conservazione del prodotto o dello zero (nel caso additivo) sono esplicitamente rappresentate e dimostrabili.

Quando si passa dai monoidi ai gruppi, si introduce l’invertibilità degli elementi. Ogni gruppo è, quindi, un monoid con un’ulteriore proprietà: per ogni elemento esiste il suo inverso. Questo consente di usare tattiche automatizzate come group in Lean, che verificano identità valide in qualsiasi gruppo libero. Inoltre, esistono morfismi di gruppi, che sono semplicemente morfismi di monoidi definiti tra gruppi. Anche qui si conserva la compatibilità con le strutture già definite.

È possibile costruire tali morfismi senza specificare esplicitamente tutte le proprietà: per esempio, un’applicazione $f : G \to H$ tra gruppi che rispetta la moltiplicazione può essere elevata a morfismo di gruppi con MonoidHom.mk'. Inoltre, le isomorfie di gruppi sono rappresentate come MulEquiv, con strumenti associati come MulEquiv.symm per l'inverso e MulEquiv.trans per la composizione.

Importante è anche la possibilità di costruire isomorfismi a partire da morfismi bijettivi grazie a MulEquiv.ofBijective. In tal caso, però, si entra nel dominio della non computabilità, una distinzione rilevante nell’ambito della formalizzazione rigorosa.

I sottogruppi non sono semplici predicati, ma strutture a sé stanti del tipo Subgroup G, dotate di coercizione automatica a insiemi di $G$. Questo consente l’utilizzo diretto dell’appartenenza con ∈ e l’uso di proprietà come la ch