Απόδειξη θεωρημάτων/προβλημάτων από μηχανή

[Τσιαλας Νικολαος]

Καλησπέρα σε όλους!Εύχομαι καλά αποτελέσματα και στις 2 ομάδες μας! Κάπου διάβασα ότι του χρόνου στην IMO2021 η microsoft θα "κατεβάσει" υπολογιστή σαν διαγωνιζόμενο ... Γνωρίζει κάποιος αν ισχύει αυτό?

Επεξεργασία από Demetres: Έγινε μεταφορά αναρτήσεων από τη συζήτηση για τα θέματα της IMO σε αυτό το πιο σχετικό θέμα.

[miltosk]

Καλησπέρα σε όλους!Εύχομαι καλά αποτελέσματα και στις 2 ομάδες μας! Κάπου διάβασα ότι του χρόνου στην IMO2021 η microsoft θα "κατεβάσει" υπολογιστή σαν διαγωνιζόμενο ... Γνωρίζει κάποιος αν ισχύει αυτό?

Καλά αποτελέσματα στις ομάδες μας και από εμένα.
Κάτι λένε στο aops. Αλλά δεν νομίζω να είναι διαγωνιζόμενος. Εξάλλου όλοι ξέρουμε ότι ένας υπολογιστής, και δη της Microsoft που έχει τόσο χρήμα, μπορεί να έχει πολύ περισσότερες δυνατότητες από έναν άνθρωπο πάνω σε ένα και μόνο συγκεκριμένο αντικείμενο. Έχουμε καμία ιδέα σε partial results ή γενικά πότε θα βγουν?

[Τσιαλας Νικολαος]

Τελικά μάλλον ισχύει...

https://imo-grand-challenge.github.io/

Για τα αποτελέσματα δεν γνωρίζω

[mick7]

4 προβλήματα συνδιαστικης / θεωρίας αριθμών...Μετά βλέπω τα ονόματα της επιτροπής

Daniel Selsam (Microsoft Research)
Leonardo de Moura (Microsoft Research)
Sarah Loos (Google AI)

Τυχαίο ?

[Demetres]

4 προβλήματα συνδιαστικης / θεωρίας αριθμών...Μετά βλέπω τα ονόματα της επιτροπής

Daniel Selsam (Microsoft Research)
Leonardo de Moura (Microsoft Research)
Sarah Loos (Google AI)

Τυχαίο ?

Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.

[Al.Koutsouridis]

Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.

Κάτι τέτοιο φαντάστηκα όταν είδα τα ονόματα. Η επιλογή των θεμάτων περισσότερο θυμίζει παίξιμο έδρας. Καλά αποτελέσματα στην Ελληνική και Κυπριακή ομάδα. Πολλά από τα παιδιά γράφουν εδώ συχνά και θα χαρούμε να δούμε τις λύσεις τους, αν δεν δεσμεύονται από άλλους παράγοντες.

Υγ. Ξέρουμε αν η ελληνική πλευρά θα κάνει αίτηση για διαξαγωγή της επόμενης ολυμπιάδας; Είναι καλή ευκαιρία νομίζω.

[mick7]

Έχετε δίκιο...έπρεπε να το είχα διαβάσει με προσοχή...από την άλλη όμως νομίζω ότι τα προβλήματα που μπορούν να αντιμετωπιστούν "καλύτερα" από υπολογιστές είναι ακριβώς αυτά της συνδυαστικής / θεωρίας αριθμών.

Υπάρχει μια παρανόηση. Τα άτομα αυτά δεν ήταν στην επιτροπή επιλογής των προβλημάτων για ΙΜΟ. Αντίθετα είναι μέλη της επιτροπής για κατασκευή τεχνητής νοημοσύνης η οποία να μπορεί να λύνει προβλήματα αυτών των διαγωνισμών.

[george visvikis]

Ας αφήσουν τους ανθρώπους να διαγωνίζονται με ανθρώπους και τους υπολογιστές με υπολογιστές.

Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;

[Al.Koutsouridis]

Ας αφήσουν τους ανθρώπους να διαγωνίζονται με ανθρώπους και τους υπολογιστές με υπολογιστές.

Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;

Όχι απαραίτητα. Μπορεί να γίνει αναγωγή στους κανόνες της λογικής και τα αξιώματα της γεωμετρίας.

[mick7]

O υπολογιστής μπορεί να αντιμετωπίσει ένα οποιοδήποτε πρόβλημα εάν μεταφραστεί στην "γλώσσα" του. Φαντάζομαι εάν γεωμετρικό πρόβλημα μεταφραστεί με ορούς αναλυτικής γεωμετρίας δηλαδή κατά ουσίαν Άλγεβρας και πιο συγκεκριμένα πολυωνύμων τότε ίσως μπορεί να λυθεί.
Φαντάζομαι ότι έτσι δουλεύει το GPS, το Google Maps και άλλα.
Υπάρχει ολόκληρος κλάδος που ασχολείται με την διεπαφή υπολογιστών και Γεωμετρίας η υπολογιστική γεωμετρία.

https://en.wikipedia.org/wiki/Computational_geometry

Ας αφήσουν τους ανθρώπους να διαγωνίζονται με ανθρώπους και τους υπολογιστές με υπολογιστές.

Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;

[Al.Koutsouridis]

O υπολογιστής μπορεί να αντιμετωπίσει ένα οποιοδήποτε πρόβλημα εάν μεταφραστεί στην "γλώσσα" του. Φαντάζομαι εάν γεωμετρικό πρόβλημα μεταφραστεί με ορούς αναλυτικής γεωμετρίας δηλαδή κατά ουσίαν Άλγεβρας και πιο συγκεκριμένα πολυωνύμων τότε ίσως μπορεί να λυθεί.
Φαντάζομαι ότι έτσι δουλεύει το GPS, το Google Maps και άλλα.
Υπάρχει ολόκληρος κλάδος που ασχολείται με την διεπαφή υπολογιστών και Γεωμετρίας η υπολογιστική γεωμετρία.

https://en.wikipedia.org/wiki/Computational_geometry

Δεν έχουν σχέση τα παραπάνω με την απόδειξη των γεωμετρικών προβλημάτων από μηχανή.

[DrStrange]

Ας αφήσουν τους ανθρώπους να διαγωνίζονται με ανθρώπους και τους υπολογιστές με υπολογιστές.

Αλήθεια, πώς μπορεί ένας υπολογιστής να αντιμετωπίσει ένα γεωμετρικό πρόβλημα;
Μήπως θα χρησιμοποιεί μιγαδικούς για να αποδείξει μία απλή σχέση ισότητας;

Δεν νομίζω ότι έχουμε κάτι να φοβηθούμε. Ίσα ίσα, νομίζω στην συγκεκριμένη μάχη ανθρώπου-μηχανής , θα νικήσει ο άνθρωπος. Κάθε χρόνο υπάρχουν άτομα που παίρνουν perfect-score αυτό μόνο αρκεί.

[miltosk]

Νομίζω έχει ξεφύγει λίγο η συζήτηση από το θέμα.
Τώρα επί της συζήτησης αν δώσω το παράδειγμα μιγαδικής γεωμετρίας (που αναφέρεται από τον κ.Βισβίκη πιο πάνω) όπου το πρόβλημα είναι οι πράξεις, νομίζω ότι ένας υπολογιστής έχει μεγάλο προβάδισμα.

[mick7]

Εξαρτάται πως ορίζουμε ένα γεωμετρικό πρόβλημα πχ "η ελάχιστη απόσταση που πρέπει να διανύσουμε για να φτάσουμε σε ενα σημείο στον αστικό ιστό" Αν αναφερόμαστε στο επίπεδο σχολικής γεωμετρίας ήτοι Ευκλείδειας όντως νομίζω οτι δεν υπάρχει εργαλείο που να δίνει αυτόματες (μηχανικές) αποδείξεις ακόμη.Βέβαια, για να υπάρξει έρευνα πρέπει να υπάρχουν και αντίστοιχα κεφάλαια τα οποία προφανώς θα προέρχονται από την ανάγκη να λυθούν προβλήματά που αντιμετωπίζει μεγάλο μέρος μια κοινωνίας. Τα προβλήματά της Ευκλείδης Γεωμετρίας και αν λύνονται υπολογιστικά δεν νομίζω ότι απασχολεί τους περισσοτέρους.
Φαντάζομαι σαν μηχανικός κατέχετε καλύτερα το R&D.

Δεν έχουν σχέση τα παραπάνω με την απόδειξη των γεωμετρικών προβλημάτων από μηχανή.

[Al.Koutsouridis]

Με αφορμή την συζήτηση στο νήμα https://mathematica.gr/forum/viewtopic.php?f=58&t=67947 μεταφέρω την συζήτηση εδώ για να μείνει το αναφερθέν στο σκοπό του. Η επιμελητές μπορούν να μεταφέρουν τα εκτός θέματος μηνύματα εδώ.

[Μάρκος Βασίλης]

Σε ό,τι αφορά το ζήτημα των διαγωνισμών θα ήταν άδικο να συμμετέχουν υπολογιστές διαγωνιστικά, ωστόσο θα ήταν πολύ χρήσιμο ερευνητικά να επιτρέπουμε σε τέτοιες εφαρμογές να επιλύουν τα προβλήματα live την ώρα που το κάνουν και οι διαγωνιζόμενοι/ες.

Σε σχέση τώρα με τις αποδείξεις θεωρημάτων της Ευκλείδειας γεωμετρίας, υπάρχουν πολλές τεχνικές που βασίζονται είτε σε άλγεβρα - μέσω πολυωνύμων αλλά και γεωμετρικών μετασχηματισμών (Klein) - είτε σε αξιωματικές προσεγγίσεις όπως π.χ. μέσω των αξιωμάτων του Tarski, του Hilbert ή υποσυνόλων/παραλλαγών τους. Μάλιστα στη δεύτερη κατηγορία υπάρχουν προσεγγίσεις που υιοθετούν προσεγγίσεις που βασίζονται σε resolution () ή προσεγγίσεις που βασίζονται σε κατασκευαστικές/ιντουισιονιστικές προσεγγίσεις.

Γενικά η Ευκλείδεια γεωμετρία είναι από τα πρόσφορα πεδία για να ασχοληθεί κανείς σε ό,τι αφορά τις αξιωματικές προσεγγίσεις μιας και η θεωρία της μπορεί να εκφραστεί όλη σε πρωτοβάθμια λογική - έστω και με ένα μη πεπερασμένο σύνολο αξιωμάτων.