Discussion:
Math всё
(слишком старое сообщение для ответа)
Vulcan
2024-07-25 16:19:26 UTC
Permalink
AI achieves silver-medal standard solving International Mathematical
Olympiad problems

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
somnambulic
2024-07-25 17:37:44 UTC
Permalink
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
большинство современных теорем публикуются с ошибками. никто не читает
доказательств. если что-то знаковое то череда коррекций. это я про
алгоритмы, в математике вроде та же хрень. если еще ии нагенерирует
доказательств вагон ой.
Vulcan
2024-07-25 19:13:48 UTC
Permalink
Post by somnambulic
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
большинство современных теорем публикуются с ошибками. никто не читает
доказательств. если что-то знаковое то череда коррекций. это я про
мне вот тоже любопытен этот аспект

сыновья опуликовали по нескольку работ в TCS/Math

из рецензией не всегда очевидно, осилил ли рецензент доказательства)
Post by somnambulic
алгоритмы, в математике вроде та же хрень. если еще ии нагенерирует
доказательств вагон ой.
AI докажет, AI же и проверит

"AlphaProof is a system that trains itself to prove mathematical
statements in the formal language Lean. It couples a pre-trained
language model with the AlphaZero reinforcement learning algorithm,
which previously taught itself how to master the games of chess, shogi
and Go.

Formal languages offer the critical advantage that proofs involving
mathematical reasoning can be formally verified for correctness. Their
use in machine learning has, however, previously been constrained by the
very limited amount of human-written data available.

In contrast, natural language based approaches can hallucinate plausible
but incorrect intermediate reasoning steps and solutions, despite having
access to orders of magnitudes more data. We established a bridge
between these two complementary spheres by fine-tuning a Gemini model to
automatically translate natural language problem statements into formal
statements, creating a large library of formal problems of varying
difficulty.

When presented with a problem, AlphaProof generates solution candidates
and then proves or disproves them by searching over possible proof steps
in Lean. Each proof that was found and verified is used to reinforce
AlphaProof’s language model, enhancing its ability to solve subsequent,
more challenging problems."
somnambulic
2024-07-25 19:30:29 UTC
Permalink
Post by Vulcan
Post by somnambulic
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
большинство современных теорем публикуются с ошибками. никто не читает
доказательств. если что-то знаковое то череда коррекций. это я про
мне вот тоже любопытен этот аспект
сыновья опуликовали по нескольку работ в TCS/Math
из рецензией не всегда очевидно, осилил ли рецензент доказательства)
Post by somnambulic
алгоритмы, в математике вроде та же хрень. если еще ии нагенерирует
доказательств вагон ой.
AI докажет, AI же и проверит
"AlphaProof is a system that trains itself to prove mathematical
statements in the formal language Lean. It couples a pre-trained
language model with the AlphaZero reinforcement learning algorithm,
which previously taught itself how to master the games of chess, shogi
and Go.
Formal languages offer the critical advantage that proofs involving
mathematical reasoning can be formally verified for correctness. Their
use in machine learning has, however, previously been constrained by the
very limited amount of human-written data available.
In contrast, natural language based approaches can hallucinate plausible
but incorrect intermediate reasoning steps and solutions, despite having
access to orders of magnitudes more data. We established a bridge
between these two complementary spheres by fine-tuning a Gemini model to
automatically translate natural language problem statements into formal
statements, creating a large library of formal problems of varying
difficulty.
When presented with a problem, AlphaProof generates solution candidates
and then proves or disproves them by searching over possible proof steps
in Lean. Each proof that was found and verified is used to reinforce
AlphaProof’s language model, enhancing its ability to solve subsequent,
more challenging problems."
Сон-про-несон-не-сон-просон
Vulcan
2024-07-25 19:58:26 UTC
Permalink
Post by somnambulic
Post by Vulcan
When presented with a problem, AlphaProof generates solution candidates
and then proves or disproves them by searching over possible proof steps
in Lean. Each proof that was found and verified is used to reinforce
AlphaProof’s language model, enhancing its ability to solve subsequent,
more challenging problems."
Сон-про-несон-не-сон-просон
/погуглив/ да, как-то так
G
2024-07-25 17:48:19 UTC
Permalink
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
--
G
Vulcan
2024-07-25 19:23:31 UTC
Permalink
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга

ну и вот...
D
2024-07-25 19:59:10 UTC
Permalink
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
Это если экзаменуемый не сталкивался с этой задачкой раньше.

А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад


Bye, Anatol
Vulcan
2024-07-25 20:04:29 UTC
Permalink
Post by D
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад
I tried this year’s problems while I was at the International #Math
Olympiad myself. It took me hours. I imagine that when people saw
Sputnik overhead in 1957, they might have had the same feeling that I do
now.

I have been anticipating this level of #AI coming, but thought it was
still years away. My interest is not in making AI better, but in what we
need to do to help all the people. That’s below.

But first, context: IMO problems are specifically selected to be
non-standard. For the previous 10 years, I served as the national coach
of the USA International Math Olympiad team
(https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During the
IMO itself, the national coaches meet to select the problems that will
appear on the exam paper.
One of the most important tasks of that group is to avoid problems that
have similarity to problems that have appeared anywhere before. During
those meetings, national coaches would often dig up an old obscure math
competition, on which a similar problem had appeared, and show it to the
group, after which the proposed problem would be struck down.

So, this AI breakthrough is totally different from #GPT being able to do
standardized tests through pattern-matching. It strikes at the heart of
discovery. It's very common for students to hit a wall the first time
they try IMO-style problems, because they are accustomed to learning
from example, remembering, and executing similar steps.

Take a look at the 6 problems for yourself, and you’ll see that they are
way beyond any curricular standards:
https://www.imo-official.org/year_info.aspx?year=2024. And even though
the AI took more than the normal time limit, it’s only a matter of time
before the software and hardware speed up, so the sheer fact that it was
able to solve the problems at all is a major advance. The hard part of
solving these problems isn’t calculation. It’s inventing a solution
pathway. Most people would get 0 points even if they had a year to think.

Now what does this mean for people? And what can we actually do about it?

https://url.vulakh.us/loh

кто такой Po-Shen Loh объяснять не надо?

или надо?
D
2024-07-26 11:24:28 UTC
Permalink
Post by Vulcan
Post by D
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад
I tried this year’s problems while I was at the International #Math
Olympiad myself. It took me hours. I imagine that when people saw
Sputnik overhead in 1957, they might have had the same feeling that I do
now.
I have been anticipating this level of #AI coming, but thought it was
still years away. My interest is not in making AI better, but in what we
need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be
non-standard. For the previous 10 years, I served as the national coach
of the USA International Math Olympiad team
10 лет - а олимпиады дольше проводят.
И все что он "придумывает" - в каких нибудь других учебниках/источниках
описано.

Математика же не изобретает ничего, а просто тип с шизофренией черкает
каракули на салфетке, которые понимают два-три человека с таким же
диагнозом, а "результаты" никакого практического значения не имеют.

Bye, Anatol

"Гай рассказал о чисто абстрактной математической теории,
рассматривавшей Мир иначе. Теория эта возникла еще в античные времена,
преследовалась некогда официальной религией, имела своих мучеников,
получила математическую стройность трудами гениальных математиков
прошлого века, но так и осталась чисто абстрактной, хотя, как и
большинство абстрактных теорий, нашла себе наконец практическое
применение - совсем недавно, когда были созданы сверхдальнобойные
баллистические снаряды."
Vulcan
2024-07-26 15:21:53 UTC
Permalink
Post by D
Post by Vulcan
Post by D
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад
I tried this year’s problems while I was at the International #Math
Olympiad myself. It took me hours. I imagine that when people saw
Sputnik overhead in 1957, they might have had the same feeling that I
do now.
I have been anticipating this level of #AI coming, but thought it was
still years away. My interest is not in making AI better, but in what
we need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be
non-standard. For the previous 10 years, I served as the national
coach of the USA International Math Olympiad team
10 лет - а олимпиады дольше проводят.
И все что он "придумывает" - в каких нибудь других учебниках/источниках
описано.
чукча не читатель?

"One of the most important tasks of that group is to avoid problems that
have similarity to problems that have appeared anywhere before. During
those meetings, national coaches would often dig up an old obscure math
competition, on which a similar problem had appeared, and show it to the
group, after which the proposed problem would be struck down."
Post by D
Математика же не изобретает ничего, а просто тип с шизофренией черкает
каракули на салфетке, которые понимают два-три человека с таким же
диагнозом, а "результаты" никакого практического значения не имеют.
ты так говоришь, как будто это что-то плохое
Post by D
"Гай рассказал о чисто абстрактной математической теории,
рассматривавшей Мир иначе. Теория эта возникла еще в античные времена,
преследовалась некогда официальной религией, имела своих мучеников,
получила математическую стройность трудами гениальных математиков
прошлого века, но так и осталась чисто абстрактной, хотя, как и
большинство абстрактных теорий, нашла себе наконец практическое
применение - совсем недавно, когда были созданы сверхдальнобойные
баллистические снаряды."
да, это вечная история

Hardy preferred his work to be considered pure mathematics, perhaps
because of his detestation of war and the military uses to which
mathematics had been applied. He made several statements similar to that
in his Apology:

I have never done anything "useful". No discovery of mine has made, or
is likely to make, directly or indirectly, for good or ill, the least
difference to the amenity of the world.

However, aside from formulating the Hardy–Weinberg principle in
population genetics, his famous work on integer partitions with his
collaborator Ramanujan, known as the Hardy–Ramanujan asymptotic formula,
has been widely applied in physics to find quantum partition functions
of atomic nuclei (first used by Niels Bohr) and to derive thermodynamic
functions of non-interacting Bose–Einstein systems. Though Hardy wanted
his maths to be "pure" and devoid of any application, much of his work
has found applications in other branches of science.

Moreover, Hardy deliberately pointed out in his Apology that
mathematicians generally do not "glory in the uselessness of their
work," but rather – because science can be used for evil ends as well as
good – "mathematicians may be justified in rejoicing that there is one
science at any rate, and that their own, whose very remoteness from
ordinary human activities should keep it gentle and clean."

https://en.wikipedia.org/wiki/G._H._Hardy
Sergey Babkin
2024-07-26 23:34:04 UTC
Permalink
Post by D
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад
I tried this year’s problems while I was at the International #Math Olympiad
myself. It took me hours. I imagine that when people saw Sputnik overhead in
1957, they might have had the same feeling that I do now.
I have been anticipating this level of #AI coming, but thought it was still
years away. My interest is not in making AI better, but in what we need to do to
help all the people. That’s below.
But first, context: IMO problems are specifically selected to be non-standard.
For the previous 10 years, I served as the national coach of the USA
International Math Olympiad team
(https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During the IMO
itself, the national coaches meet to select the problems that will appear on the
exam paper.
One of the most important tasks of that group is to avoid problems that have
similarity to problems that have appeared anywhere before. During those
meetings, national coaches would often dig up an old obscure math competition,
on which a similar problem had appeared, and show it to the group, after which
the proposed problem would be struck down.
So, this AI breakthrough is totally different from #GPT being able to do
standardized tests through pattern-matching. It strikes at the heart of
discovery. It's very common for students to hit a wall the first time they try
IMO-style problems, because they are accustomed to learning from example,
remembering, and executing similar steps.
Take a look at the 6 problems for yourself, and you’ll see that they are way
https://www.imo-official.org/year_info.aspx?year=2024. And even though the AI
took more than the normal time limit, it’s only a matter of time before the
software and hardware speed up, so the sheer fact that it was able to solve the
problems at all is a major advance. The hard part of solving these problems
isn’t calculation. It’s inventing a solution pathway. Most people would get 0
points even if they had a year to think.
Now what does this mean for people? And what can we actually do about it?
https://url.vulakh.us/loh
кто такой Po-Shen Loh объяснять не надо?
или надо?
Кто такой этото Лох - я не знаю, но вот до меня только что дошло, что это
наконец-то реализация комбинированного интеллекта. Идея по сути довольно
простая: вот, скажем, считать до 100 - для человека довольно сложная задача,
дети ей учатся годами. А компьютер может это делать очень легко и эффективно.
Поэтому пытаться научить компьютерный ИИ арифметике - глупо и неэффективно. От
этого происходят не только тормоза, но и косяки в арифметике ("галлюцинации").
Вместо того надо сращивать ИИ и родную реализацию арифметики в компьютере, по
сути мозг со встроенным нейроинтерфейсом к калькулятору. То же самое относится к
многим другим областям - грамматики, логические доказательства, и прочее.

Мне уже лет 10 как непонятно, почему так не сращивают. Я тогда увидел пример,
который пытается научить ИИ находить соответствие количества открывающих и
закрывающих скобок, с попыткой разобрать, что там получилось в индивидуальных
нейронах - типа, этот реагирует на открывание, этот на открывание, а тут
считается баланс, но кривовато. И подумал, что было бы очень логично отдать
подсчет в отдельную арифметическую логику, к которой обращаться из нейронной сети.

И вот наконец-то на практике сростили.

-СБ
hedin
2024-07-27 10:49:50 UTC
Permalink
Post by Sergey Babkin
Post by Vulcan
Post by D
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет олимпиад
I tried this year’s problems while I was at the International #Math
Olympiad myself. It took me hours. I imagine that when people saw
Sputnik overhead in 1957, they might have had the same feeling that I
do now.
I have been anticipating this level of #AI coming, but thought it was
still years away. My interest is not in making AI better, but in what
we need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be
non-standard. For the previous 10 years, I served as the national
coach of the USA International Math Olympiad team
(https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During
the IMO itself, the national coaches meet to select the problems that
will appear on the exam paper.
One of the most important tasks of that group is to avoid problems
that have similarity to problems that have appeared anywhere before.
During those meetings, national coaches would often dig up an old
obscure math competition, on which a similar problem had appeared, and
show it to the group, after which the proposed problem would be struck
down.
So, this AI breakthrough is totally different from #GPT being able to
do standardized tests through pattern-matching. It strikes at the
heart of discovery. It's very common for students to hit a wall the
first time they try IMO-style problems, because they are accustomed to
learning from example, remembering, and executing similar steps.
Take a look at the 6 problems for yourself, and you’ll see that they
https://www.imo-official.org/year_info.aspx?year=2024. And even though
the AI took more than the normal time limit, it’s only a matter of
time before the software and hardware speed up, so the sheer fact that
it was able to solve the problems at all is a major advance. The hard
part of solving these problems isn’t calculation. It’s inventing a
solution pathway. Most people would get 0 points even if they had a
year to think.
Now what does this mean for people? And what can we actually do about it?
https://url.vulakh.us/loh
кто такой Po-Shen Loh объяснять не надо?
или надо?
Кто такой этото Лох - я не знаю, но вот до меня только что дошло, что
это наконец-то реализация комбинированного интеллекта. Идея по сути
довольно простая: вот, скажем, считать до 100 - для человека довольно
сложная задача, дети ей учатся годами. А компьютер может это делать
очень легко и эффективно. Поэтому пытаться научить компьютерный ИИ
арифметике - глупо и неэффективно. От этого происходят не только
тормоза, но и косяки в арифметике ("галлюцинации"). Вместо того надо
сращивать ИИ и родную реализацию арифметики в компьютере, по сути мозг
со встроенным нейроинтерфейсом к калькулятору. То же самое относится к
многим другим областям - грамматики, логические доказательства, и прочее.
Мне уже лет 10 как непонятно, почему так не сращивают.
Это ты просто не в курсе.
RAG называется.
И что там во внешем источнике (векторная дб или другая LLM) на самом
деле неважно
Вулкан
2024-07-28 02:29:25 UTC
Permalink
Post by hedin
Post by Sergey Babkin
Post by Vulcan
Post by D
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
Это если экзаменуемый не сталкивался с этой задачкой раньше.
А если AI для тренировки скормили задачки с решениями за 20 лет
олимпиад
I tried this year’s problems while I was at the International #Math
Olympiad myself. It took me hours. I imagine that when people saw
Sputnik overhead in 1957, they might have had the same feeling that I
do now.
I have been anticipating this level of #AI coming, but thought it was
still years away. My interest is not in making AI better, but in what
we need to do to help all the people. That’s below.
But first, context: IMO problems are specifically selected to be
non-standard. For the previous 10 years, I served as the national
coach of the USA International Math Olympiad team
(https://www.quantamagazine.org/po-shen-loh-led-the-u-s...). During
the IMO itself, the national coaches meet to select the problems that
will appear on the exam paper.
One of the most important tasks of that group is to avoid problems
that have similarity to problems that have appeared anywhere before.
During those meetings, national coaches would often dig up an old
obscure math competition, on which a similar problem had appeared,
and show it to the group, after which the proposed problem would be
struck down.
So, this AI breakthrough is totally different from #GPT being able to
do standardized tests through pattern-matching. It strikes at the
heart of discovery. It's very common for students to hit a wall the
first time they try IMO-style problems, because they are accustomed
to learning from example, remembering, and executing similar steps.
Take a look at the 6 problems for yourself, and you’ll see that they
https://www.imo-official.org/year_info.aspx?year=2024. And even
though the AI took more than the normal time limit, it’s only a
matter of time before the software and hardware speed up, so the
sheer fact that it was able to solve the problems at all is a major
advance. The hard part of solving these problems isn’t calculation.
It’s inventing a solution pathway. Most people would get 0 points
even if they had a year to think.
Now what does this mean for people? And what can we actually do about it?
https://url.vulakh.us/loh
кто такой Po-Shen Loh объяснять не надо?
или надо?
Кто такой этото Лох - я не знаю, но вот до меня только что дошло, что
это наконец-то реализация комбинированного интеллекта. Идея по сути
довольно простая: вот, скажем, считать до 100 - для человека довольно
сложная задача, дети ей учатся годами. А компьютер может это делать
очень легко и эффективно. Поэтому пытаться научить компьютерный ИИ
арифметике - глупо и неэффективно. От этого происходят не только
тормоза, но и косяки в арифметике ("галлюцинации"). Вместо того надо
сращивать ИИ и родную реализацию арифметики в компьютере, по сути мозг
со встроенным нейроинтерфейсом к калькулятору. То же самое относится к
многим другим областям - грамматики, логические доказательства, и прочее.
Мне уже лет 10 как непонятно, почему так не сращивают.
Это ты просто не в курсе.
RAG называется.
И что там во внешем источнике (векторная дб или другая LLM) на самом
деле неважно
там на самом деле все еще интереснее

см. ссылку на гугл вверху

ключевые моменты я даже процитировал
hedin
2024-07-28 14:05:06 UTC
Permalink
Post by Вулкан
там на самом деле все еще интереснее
ты даже не представляешь себе насколько :-)
Post by Вулкан
см. ссылку на гугл вверху
ключевые моменты я даже процитировал
а своими словами, для тупых?
которые прачечные абасучивают
или апачи компилируют?
AVI
2024-07-28 14:35:27 UTC
Permalink
Post by Вулкан
там на самом деле все еще интереснее
   ты даже не представляешь себе насколько :-)
Да нет там ничего интересного. В конечном итоге все эти нейросети -
это всего лишь весьма заёбистые разностные схемы и только. Что объясняет
весь их зоопарк/цирк и различия в их "тренерах".
Vulcan
2024-07-28 15:36:47 UTC
Permalink
Post by Вулкан
там на самом деле все еще интереснее
   ты даже не представляешь себе насколько :-)
Post by Вулкан
см. ссылку на гугл вверху
ключевые моменты я даже процитировал
  а своими словами, для тупых?
  которые прачечные абасучивают
  или апачи компилируют?
оно не просто генерирует решения-кандидаты, оно их ещё и пытается
формально доказать (задачи IMO требуют доказательств)

причём если удаётся доказать, то стопроцентно правильно
D
2024-07-28 17:40:03 UTC
Permalink
Post by Vulcan
   а своими словами, для тупых?
   которые прачечные абасучивают
   или апачи компилируют?
оно не просто генерирует решения-кандидаты, оно их ещё и пытается
формально доказать (задачи IMO требуют доказательств)
причём если удаётся доказать, то стопроцентно правильно
А напомните пожалуйста что такое "доказать"?
Разве "доказательство" не может быть ошибочным?



Bye, Anatol
Vulcan
2024-07-28 17:52:40 UTC
Permalink
Post by D
Post by Vulcan
   а своими словами, для тупых?
   которые прачечные абасучивают
   или апачи компилируют?
оно не просто генерирует решения-кандидаты, оно их ещё и пытается
формально доказать (задачи IMO требуют доказательств)
причём если удаётся доказать, то стопроцентно правильно
А напомните пожалуйста что такое "доказать"?
Разве "доказательство" не может быть ошибочным?
я уже цитировал relevant portions

цитирую ещё раз:

AlphaProof is a system that trains itself to prove mathematical
statements in the formal language Lean.
...
Formal languages offer the critical advantage that proofs involving
mathematical reasoning can be formally verified for correctness.
hedin
2024-07-29 15:50:28 UTC
Permalink
Post by Vulcan
Post by Вулкан
там на самом деле все еще интереснее
    ты даже не представляешь себе насколько :-)
Post by Вулкан
см. ссылку на гугл вверху
ключевые моменты я даже процитировал
   а своими словами, для тупых?
   которые прачечные абасучивают
   или апачи компилируют?
оно не просто генерирует решения-кандидаты, оно их ещё и пытается
формально доказать (задачи IMO требуют доказательств)
А, это да, оно еще и может рассказать (если попросить)
шаг за шагом как и почему
Post by Vulcan
причём если удаётся доказать, то стопроцентно правильно
А вот в это верить не надо :-)
Вулкан
2024-07-30 03:32:36 UTC
Permalink
Post by hedin
Post by Vulcan
Post by Вулкан
там на самом деле все еще интереснее
    ты даже не представляешь себе насколько :-)
Post by Вулкан
см. ссылку на гугл вверху
ключевые моменты я даже процитировал
   а своими словами, для тупых?
   которые прачечные абасучивают
   или апачи компилируют?
оно не просто генерирует решения-кандидаты, оно их ещё и пытается
формально доказать (задачи IMO требуют доказательств)
А, это да, оно еще и может рассказать (если попросить)
шаг за шагом как и почему
Post by Vulcan
причём если удаётся доказать, то стопроцентно правильно
А вот в это верить не надо :-)
хочешь - верь, не хочешь - проверь
Vulcan
2024-07-25 19:59:44 UTC
Permalink
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
ну и вот...
https://url.vulakh.us/iq
G
2024-07-25 22:02:07 UTC
Permalink
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
ну и вот...
Наличие мозга у людей, причем тут ИИ то?
И почему субж? Куда оно по твоему денется если ИИ этим займется ?
--
G
Vulcan
2024-07-26 15:23:54 UTC
Permalink
Post by G
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
ну и вот...
Наличие мозга у людей, причем тут ИИ то?
И почему субж? Куда оно по твоему денется если ИИ этим займется ?
не знаю

будем посмотреть

очевидно, грядут серьёзные изменения в том, how made is done

этот новый инструментарий посильнее вольфрамовых тулов будет
Вулкан
2024-07-26 19:17:10 UTC
Permalink
Post by Vulcan
Post by G
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
ну и вот...
Наличие мозга у людей, причем тут ИИ то?
И почему субж? Куда оно по твоему денется если ИИ этим займется ?
не знаю
будем посмотреть
очевидно, грядут серьёзные изменения в том, how made is done
*math is done
Post by Vulcan
этот новый инструментарий посильнее вольфрамовых тулов будет
G
2024-08-01 00:47:30 UTC
Permalink
Post by Vulcan
Post by G
Post by Vulcan
Post by G
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Эти олимпиады для людей были придуманы, как достижения ии повлияет на
олимпиады?
олимпиады были придуманы, чтобы проверять наличие мозга
ну и вот...
Наличие мозга у людей, причем тут ИИ то?
И почему субж? Куда оно по твоему денется если ИИ этим займется ?
не знаю
будем посмотреть
очевидно, грядут серьёзные изменения в том, how made is done
этот новый инструментарий посильнее вольфрамовых тулов будет
Я согласен, что дело крутой поворот берет, будет очень интересно в след
20-50 лет..
Однако, если про олимпиады для людей конкретно говорить, то изменений я как
то не вижу.

ИИ может долго и много чего то доказывать, робот он железный, вот только
кому до этого дело, если мало кто понимает, че он там доказывает?
--
G
YurаS
2024-07-25 19:30:05 UTC
Permalink
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
А хорошо ли это для евреев? :)
Vulcan
2024-07-25 19:58:02 UTC
Permalink
Post by YurаS
Post by Vulcan
AI achieves silver-medal standard solving International Mathematical
Olympiad problems
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
А хорошо ли это для евреев? :)
это хороший, правильный вопрос

я и сам им в последнее время задаюсь)

для пейджа с брином - хорошо

для меня - пока не уверен)

но тоже, думаю, хорошо, в конечном итоге

вкалывают роботы, а не человек, и вот это всё

https://url.vulakh.us/thematrix

а у евреев будет больше времени на изучение Торы
D
2024-07-25 20:08:39 UTC
Permalink
Post by Vulcan
а у евреев будет больше времени на изучение Торы
А разве Тору еще не скормили AI?


Согласно Торе можно ли съесть ежика в субботу?

Согласно законам кашрута, ежик не является кошерным животным и его
нельзя употреблять в пищу в любое время, включая субботу. В субботу
также существуют дополнительные ограничения на приготовление пищи,
которые делают невозможным приготовление нового блюда.




Bye, Anatol
D
2024-07-25 20:22:30 UTC
Permalink
Post by D
Post by Vulcan
а у евреев будет больше времени на изучение Торы
А разве Тору еще не скормили AI?
Согласно Торе можно ли съесть ежика в субботу?
Согласно законам кашрута, ежик не является кошерным животным и его
нельзя употреблять в пищу в любое время, включая субботу. В субботу
также существуют дополнительные ограничения на приготовление пищи,
которые делают невозможным приготовление нового блюда.
Приведи пример логического дефекта в Торе.

Тора, как и любой древний текст, может содержать моменты, которые
кажутся современному читателю нелогичными или противоречивыми. Один из
таких примеров касается закона о наказании за кражу. В книге Исход
(Шмот) 22:1 говорится, что если вор пойман при краже и убит, то его
убийца не несет ответственности. Однако в следующем стихе (22:2)
говорится, что если солнце взошло над вором, то его убийца несет
ответственность за его смерть. Это может показаться противоречивым, так
как неясно, почему время суток должно влиять на ответственность за убийство.


Bye, Anatol
Vulcan
2024-07-25 20:30:10 UTC
Permalink
Post by D
Post by D
Post by Vulcan
а у евреев будет больше времени на изучение Торы
А разве Тору еще не скормили AI?
Согласно Торе можно ли съесть ежика в субботу?
Согласно законам кашрута, ежик не является кошерным животным и его
нельзя употреблять в пищу в любое время, включая субботу. В субботу
также существуют дополнительные ограничения на приготовление пищи,
которые делают невозможным приготовление нового блюда.
Приведи пример логического дефекта в Торе.
Тора, как и любой древний текст, может содержать моменты, которые
кажутся современному читателю нелогичными или противоречивыми. Один из
таких примеров касается закона о наказании за кражу. В книге Исход
(Шмот) 22:1 говорится, что если вор пойман при краже и убит, то его
убийца не несет ответственности. Однако в следующем стихе (22:2)
говорится, что если солнце взошло над вором, то его убийца несет
ответственность за его смерть. Это может показаться противоречивым, так
как неясно, почему время суток должно влиять на ответственность за
убийство.
вот видишь, евреи всегда найдут себе занятие
Vulcan
2024-07-25 20:29:00 UTC
Permalink
Post by D
Post by Vulcan
а у евреев будет больше времени на изучение Торы
А разве Тору еще не скормили AI?
а это иррелевантно

евреи должны изучать Тору независимо от того, скормили ли её AI
Dmitry Krivitsky
2024-07-25 22:25:49 UTC
Permalink
Post by Vulcan
а у евреев будет больше времени на изучение Торы
Какой ужас.
Loading...