Alla maggior parte degli studenti,
Johannes Kepler (1571-1630) è noto per le sue
tre leggi sui moti planetari, pubblicate nell'
Astronomia nova (1609) e nell'
Harmonices mundi (1619). I suoi lavori rappresentano un tassello fondamentale della
rivoluzione scientifica, collocandosi, per così dire, sul crinale tra superstizione e metodo scientifico (ad esempio, l'
Harmonices Mundi è un sapiente mix di astronomia, musica e astrologia). Esemplare in questo senso è pure il trattatello
Strena seu de nive sixangula che nel 1611 Keplero, matematico di corte di
Rodolfo II, regalò all'amico
Johannes Matthäus Wacker von Wackenfels, a sua volta consigliere del Sacro romano imperatore, in occasione del nuovo anno. In esso l'autore, ispirato dai fiocchi di neve caduti sul suo mantello, si interroga a proposito dell'esagonalità dei cristalli che li costituiscono, intuendo per primo che essa, in qualche modo, debba essere effetto della collocazione delle sue più piccole costituenti. Ispirato dalla disposizione dei semi del melograno e delle celle all'interno di un alveare, arriva addirittura a congetturare che il problema sia analogo a quello dell'impacchettamento delle palle di cannone, formulando quella che da allora (?) è nota come
congettura di Keplero (cioè che, sostanzialmente, la disposizione più efficiente è quella impiegata sui banchi dei fruttivendoli). Il problema è tutt'altro che banale; in effetti, sono occorsi quasi quattro secoli prima che tale congettura si trasformasse in un teorema, la cui dimostrazione, largamente basata su verifiche al computer (un po' come successe con il Teorema dei quattro colori), fa decisamente storcere il naso ai puristi.
In rete è abbastanza semplice trovare in latino il testo di Keplero (
qui, ad esempio). Ho faticato un po' di più a trovarne una traduzione:
qui ce n'è una, con testo a fronte, pubblicata da Oxford nel '66.
Qui è possibile scaricare l'articolo degli
Annals che riporta la strategia impiegata nella dimostrazione originale, poi rivista integralmente
qui con l'ausilio di un software di
Automated proof checking.