ты гомик латентный

патентный

Recently, the application of AI tools to Erdos problems passed a milestone: an Erdos problem (#728 https://www.erdosproblems.com/728) was solved more or less autonomously by AI (after some feedback from an initial attempt), in the spirit of the problem (as reconstructed by the Erdos problem website community), with the result (to the best of our knowledge) not replicated in existing literature (although similar results proven by similar methods were located).

This is a demonstration of the genuine increase in capability of these tools in recent months, and is largely consistent with other recent demonstrations of AI using existing methods to resolve Erdos problems, although in most previous cases a solution to these problems was later located in the literature, as discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 . This particular case was unusual in that the problem as stated by Erdos was misformulated, with a reconstruction of the problem in the intended spirit only obtained in the last few months, which helps explain the lack of prior literature on the problem. However, I would like to talk here about another aspect of the story which I find more interesting than the solution itself, which is the emerging AI-powered capability to rapidly write and rewrite expositions of the solution. (1/5)

https://mathstodon.xyz/@tao/115855840223258103

However, I would like to talk here about another aspect of the story which I find more interesting than the solution itself, which is the emerging AI-powered capability to rapidly write and rewrite expositions of the solution.

...

But to me, the more interesting capability revealed by these events is the ability to rapidly write and rewrite new versions of a text as needed, even if one was not the original author of the argument.

This is sharp contrast to existing practice where the effort required to produce even one readable manuscript is quite time-consuming, and subsequent revisions (in response to referee reports, for instance) are largely confined to local changes (e.g., modifying the proof of a single lemma), with large-scale reworking of the paper often avoided due both to the work required and the large possibility of introducing new errors. However, the combination of reasonably competent AI text generation and modification capabilities, paired with the ability of formal proof assistants to verify the informal arguments thus generated, allows for a much more dynamic and high-multiplicity conception of what a writeup of an argument is, with the ability for individual participants to rapidly create tailored expositions of the argument at whatever level of rigor and precision is desired.

Presumably one would still want to have a singular "official" paper artefact that is held to the highest standards of writing; but this primary paper could now be accompanied by a large number of secondary alternate versions of the paper that may be somewhat looser and AI-generated in nature, but could hold additional value beyond the primary document.

Если ты посмотришь подробности по ссылке, там видно как это работает уже сейчас
Interestingly, the proof contained some minor errors in it, but the AI tool Aristotle was able to automatically repair these gaps and produce a Lean-verified proof.

и т.д.

Я не понимаю, разверните мысль пожалуйста. В посте задан вопрос про софт и математику.

Причем здесь верификация софта?

Причем здесь тогда матан, бляди тупые

>проекции

>проекции

terpi

пусть скулят и лают сатанисты

Нахуй иди

Спасибо за комментарий.

Благодарю за понимание

Эрдеш-пердеш, это ты срал у веблена?

Мартин Клеппманн голова. Я бы ему отсосал.

Спасибо за комментарий.

Нахуй иди

ну сколько лет можно повторять враньё.
не может даже писать юнит тесты для готового кода.

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

???? Глюкод это то, что создает крупномасштабную структуру и обеспечивает майнтейнабилити.
Надо наконец строить инженерную культуру в программировании, тогда и автоматизируется все лучше. Но надежды на это умерли в прошлом веке.

промпт программирование это сокращение времени на разработку

ты на ассемблере до сих пор пишешь?

В продолжение рефлексии про применение ИИ агентов в разработке. Мои личные ощущения от применения для различных задач.

Документирование. Почти на 100% закрывается с помощью ИИ агентов, при условии что сам код ясно написан и в коде документация присутствует (в Python это обязательные docstrings). Как простая документация так и сложная генерируется без излишних сложностей, но как и код её необходимо тестировать промптами в условном стиле "проверь что все примеры упомянутые в документации являются рабочими" (в реальной работе немного сложнее, но и так можно).

Тестирование. Около 90-100% тестов кода могут генерироваться автоматически, остальное с некоторой помощью. Закрывает практически все общепонятные ошибки связанные с особенностью языка и его стилистики. не закрывают какую-либо сложную логику работы с не самыми очевидными продуктами, устройствами, интеграцией и тд.

Враньё про документирование. «Агентов» не существует ввобще. Абсолютно все комментарии приходится удалять.

ну не верь, хуле я сделаю

ну я незнаю, может, заткнешься?

terpi

ПЕРЧИ!

Эйфория таки важно. И ощущение, что ты теперь можешь все, и эффект, что у тебя наконец появился коллега. Это улучшило мне трудоспособность, например, когда я впервые попытался сделать проектик в паре с ии, и я смог этот проектик закончить. Но в определенный момент раздражение начинает перевешивать эйфорию.

О, все хохлы ебаные вонючие прибежали и обмазались говном.

Ещё один быдлокодер возомонил, хехе.

Ладно, продолжай говорить на разных языках.

хуя у тебя бомбит
ИИ как раз наиболее полезен опытным профессионалам, кто знает что хочет и где потенциально могут быть косяки

хуя у тебя бомбит
ты сам-то чем занимаешься?

плагины для эклипса

Копипашка, разлогинься.

Нахуй иди

Копипашка, залогинься.

Хочешь общаться — запрещай неймфагов.

Запрещать запрещено

Банить в своем журнале — неотъемлемая свобода.

сорян что слово матан привело тебя в такое состояние ажитации, но iskramivpeople таки полностью прав

извини за выбор слов

О, все хохлы ебаные вонючие прибежали и обмазались говном.

хуя у тебя бомбит
ИИ как раз наиболее полезен опытным профессионалам, кто знает что хочет и где потенциально могут быть косяки

копипашка, привет

terpi

ПЕРЧИ!

Ладно, продолжай говорить на разных языках.

как же у русни пригорает от пруверов и ИИ

Российский математик решил задачу, 192 года считавшуюся нерешаемой

Почти два века математики считали, что для одного из самых «рабочих» классов уравнений — тех, которыми описывают движение, колебания, распространение сигналов и вообще любые меняющиеся во времени процессы — не существует универсальной формулы решения в привычном смысле. Российский математик Иван Ремизов (НИУ ВШЭ в Нижнем Новгороде и ИППИ РАН) нашёл способ обойти этот исторический тупик: он вывел общую формулу для решений дифференциальных уравнений второго порядка с переменными коэффициентами — задач, которые с 1834 года считались «безнадёжно неразрешимыми» аналитически.

https://hightech.plus/2026/01/28/rossiiskii-matematik-reshil-zadachu-192-goda-schitavshuyusya-nereshaemoi

автор этого высера мразь и говноед, а тот быдлоголовый выродок,
который эту срань сюда принес, полное и ничтожество и мразь

а с подобного заявления текст может начать только профессиональный
пропагандист, причем читатель, который на подобное покупается,
это полное днище из днища

в общем, убейте себя быстро, решительно, вы кусок говна и
вам нечего делать в этом мире