Но как-то немного грустно становится от осознания того факта, что я вот экспериментально обнаружил и теоретически доказал одну теоремку
(насколько я понимаю, ранее не доказанную, может по причине "неуловимого Джо", хотя я на основе нее оптимизировал известный "оптимальный алгоритм"), а послезавтра Стивен научит компьютер выдавать такие теоремки и даже целые абстрактные теории на гора в изобилии, а я как секретарша в конце прошлого века тупо руками перепечатывал на машинке листы или как инженер тупо считал на калькуляторе/логарифмической линейке, а сейчас компьютер сделает то же самое и быстрее и лучше. Что думаете, профессионалы?
Все это давно существует и не работает, по нескольким причинам.
Основная объективная причина - вычислительная сложность поиска доказательства (современная математика на несколько порядков сложнее того примера с булевой алгеброй о которой говорит Вольфрам. Программы, которые выводят или опровергают теоремы этого уровня, давно есть, напр. Prover9). Впрочем, Вольфрам известен тем, что игнорирует чужие исследования в области сложности.
Основная философская причина - это неформализованность понятия "интересного результата" (опять же, пример Вольфрама единичен и слишком прост - он не показывает, например, как выделять новые полезные понятия, что является вещью очень важной)
Программы, которые помогают писать и проверять формальные доказательства, уже тоже давно есть, но они не избавляют математика от работы.