Моё утверждение касалось тоталити-чекера в этих языках. В Idris по крайней мере он не даёт написать либо функцию не сокращающуюся по хотя бы одному аргументу, либо не выдающую полезное каждый шаг бесконечного вычисления.
Тоталити-чекер конечно можно отключить, но на уровне типов все функции обязаны быть тотальными
Ну и разумеется тотальное подмножество Идриса не тьюринг-полное.
В Coq и Lean думаю похоже, так как они суть вариации на ту же тему хоть и на исчислении конструкций, вместо Мартин-Лёфа
Не знаю кто был первее, но уже и Радио-Т в свой чат добавили ChatGPT. Но я всё же про то, что активные пользователи зачастую сидят в других местах. Поэтому у вас активность и не особо большая
Многие кому нужен ChatGPT уже разбежались по you.com, poe.com, utopia messendger и другим телеграмм ботам. Я вот добавился чисто для того чтоб был резерв
Моё утверждение касалось тоталити-чекера в этих языках. В Idris по крайней мере он не даёт написать либо функцию не сокращающуюся по хотя бы одному аргументу, либо не выдающую полезное каждый шаг бесконечного вычисления.
Тоталити-чекер конечно можно отключить, но на уровне типов все функции обязаны быть тотальными
Ну и разумеется тотальное подмножество Идриса не тьюринг-полное.
В Coq и Lean думаю похоже, так как они суть вариации на ту же тему хоть и на исчислении конструкций, вместо Мартин-Лёфа
Хоть убейте не могу найти здесь мат в 1 ход. И вернуться туда увы тоже не могу
Вот для заметок гораздо лучше емаксовский org-mode :)
ChatGPT на GPT-4V с плагином Wolfram не подходит?
Это комментарий от такого же новичка как и я )
Прямо в статье же прекрасный ответ на этот вопрос
А есть возможность в боте подключить плагин?
Вообще можно и на питоне, только используя биндинги для солверов типа z3
Только предупредить что хоть на poe.com и не особо доступен ChatGPT, но Sage ничуть не хуже.
Не знаю кто был первее, но уже и Радио-Т в свой чат добавили ChatGPT. Но я всё же про то, что активные пользователи зачастую сидят в других местах. Поэтому у вас активность и не особо большая
Многие кому нужен ChatGPT уже разбежались по you.com, poe.com, utopia messendger и другим телеграмм ботам. Я вот добавился чисто для того чтоб был резерв
Но ведь Sage, также как и ChatGPT работает на gpt-3,5-turbo. Или тестировали ChatGPT-4?
Странно сейчас читать мартовскую новость. Особенно учитывая что теперь плагины можно делать самим вот так https://writings.stephenwolfram.com/2023/04/instant-plugins-for-chatgpt-introducing-the-wolfram-chatgpt-plugin-kit/
А почему не Lean4?
Математика очень абстрактная штука. А у нейронок пока с абстракциями плохо
Когда стоит цель показать как переписать на rust, то да никого не волнует. А реальный код вполне мог быть неподъёмен для numba
Если бы кто-то тогда знал про AlphaGo...