Stacking oranges

inglesOriginal de

David P. Sanders, UNAM

What’s the best way to stack oranges? Go to a market, and you’ll see that any grocer knows the answer: start with a layer that looks like a honeycomb, with each orange surrounded by 6 others arranged in a hexagon, and carry on by filling in the gaps. Then keep on adding hexagonal layers, one on top of the other; that’s all there is to it. But is there really no better solution, a way for the oranges to fill a larger proportion of space?

Johannes Kepler (better known for discovering “laws” of planetary motion) conjectured in 1611 that the grocer’s method is the best, but it was not until some 400 years later, in August 2014, that a proof was finally announced, by a team of researchers led by Thomas Hales, a mathematician at the University of Pittsburgh.

This is one of a growing number of areas in mathematics in which computers have been used in a fundamental way to prove theorems. Mathematical results are turned into statements in a specially-designed computer language, which is used by computer programs called proof assistants. For example the HOL Light system used by Hales. These verify that the results follow logically from the axioms (fundamental statements) of mathematics.

Even though computers are much more trustworthy with such complicated sequences of operations than human mathematicians, and so proofs verified in this way are more certain to be correct, we humans won’t be out of a job very soon — somebody  has to come up with ideas which should be proved, and artificial intelligence still seems to be a long way off.


Empiler des oranges

francesTraducción de

Denis Boyer, UNAM

Quelle est la meilleure façon d’empiler des oranges? Allez au marché et vous verrez que tout marchand connaît la réponse: commencez avec une couche en nid d’abeilles, où chaque orange est entourée de six autres, et continuez en comblant les espaces. Ensuite, ajoutez des couches hexagonales les unes au dessus des autres, et c’est fait. Mais n’y a-t-il pas de meilleure solution, une manière d’arranger les oranges qui remplisse l’espace de  façon plus compacte?

Johannes Kepler (mieux connu pour avoir découvert les “lois” des mouvements des planètes) a conjecturé en 1611 que la méthode du marchand est la meilleure, mais ce n’est que 400 ans après, en août 2014, que la démonstration fut annoncée par une équipe de chercheurs sous la direction de Thomas Hales, un mathématicien de l’Université de Pittsburgh.

Il s’agit de l’un des nombreux domaines des mathématiques où les ordinateurs sont utilisés fondamentalement pour démontrer des théorèmes. Les résultats mathématiques sont traduits en affirmations dans un langage informatique spécialement conçu, qui est utilisé par des programmes appelés assistants de démonstration. Par exemple, le système HOL Light utilisé par Hales. Ces programmes vérifient que les résultats dérivent logiquement des axiomes des mathématiques (ou affirmations fondamentales).

Bien que les ordinateurs soient bien plus confiables que les mathématiciens humains pour manipuler des séquences si compliquées, et que les démonstrations ainsi vérifiées soient plus certainement correctes, nous les humains ne resteront pas inactifs pour demain: l’idée à démontrer doit bien venir de quelqu’un, et l’intelligence artificielle est encore loin d’en être là.

 


Apilando naranjas

 espanolTraducción de

Carlos Samuel Ruiz Vargas, ETH, Suiza

¿Cuál es la mejor forma de apilar naranjas? Vaya el lector a un mercado y verá que el dueño de cualquier puesto de naranjas lo sabe bien. En efecto: el vendedor acomoda primero una capa de naranjas en forma hexagonal (como celdas de abejas), en la cual cada naranja está rodeada por otras seis. Luego apila una segunda capa poniendo naranjas en los huecos que quedan. La segunda capa, la tercera, etc., también son hexagonales. ¿Hay alguna otra forma más compacta que esta?

Johannes Kepler (el mismo a quien debemos las tres leyes sobre el movimiento planetario) conjeturó en 1611 que el método del tendero es en efecto el mejor. Sin embargo, no fue sino hasta agosto del 2014 que se anunció, por un equipo de matemáticos liderados por Thomas Hales de la Universidad de Pittsburgh, que la conjetura de Kepler es correcta (es decir, ya es un teorema).

Este es un ejemplo del creciente número de problemas en donde las computadoras han sido usadas para probar teoremas muy complicados. Los resultados matemáticos se convierten en axiomas; en un lenguaje computacional especialmente diseñado para  llevar a cabo ciertas pruebas (como si fuera un asistente). Un lenguaje como este, llamado HOL Light system, que verifica que los resultados obtenidos se siguen lógicamente de axiomas, fue el usado por Hales.

Aun cuando las computadoras son mucho más confiables para realizar secuencias de operacions más complejas que las humanas, y por lo tanto las pruebas realizadas por ellas deberían ser correctas, nosotros los humanos no perderemos muy pronto nuestro trabajo. Alguien tiene que proveer ideas o conjeturas para ser probadas y la inteligencia artificial se ve aún muy lejana para hacerlo. C2

Sobre el autor

Deja un Comentario

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *