#theoremprover — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #theoremprover, aggregated by home.social.
-
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#HackerNews #Lean4 #AI #TheoremProver #CompetitiveEdge #MachineLearning
-
At this morning's opening session of the code4math opening (https://preview.scholarlattice.org/collections/5cc2bc74-14a7-4c27-8989-34ba88de9580), I learned that in LEAN one can prove the following theorem:
There exists a natural number a such that a - (a + 1) = 0.
The proof in LEAN is very simple: tell it to use 0. What happens behind the scenes is that, in LEAN, 0 - 1 = 0 (when considered in natural numbers). I think this is because it's convenient to have naturals closed under basic operations.
Can one then show that 1 = 2, say by manipulating a - (a + 1) = 0 into a = a + 1, adding 1 to both sides, and subtracting a? No! The reason why is that LEAN knows that subtraction in the naturals isn't subtractive. (Or rather it doesn't think that it is subtractive).
-
I should write a #TheoremProver in #Go.
For the record, I have no idea what I’m doing, how they work, or where to start, but I’ve got an idea that needs one as a component. That’s why I should write one.
-
Lol, ChatGPT предлагает мне, чтобы практиковаться в Agda следующее
> Решать задачи: Как и при изучении любого другого языка, практика очень важна. Вы можете решать задачи на sites, таких как Codewars или HackerRank, а также использовать ресурсы, такие как "The Agda Wiki", который предлагает ряд задач для решения.
Я сначала посмеялся, лет 5 назад я заходил на этот прекрасный сайт, кажется агдой там и не пахло, а сейчас захожу и там есть специальные задачи для Agda. Я в шоке. Сук, всё. Challenge accepted.
-
Ich arbeite gerade an einer Einführung in die mathematische #Modellierung mit dem #TheoremProver #IsabelleHOL am Beispiel #Philosophie
Die ersten ~70 Seiten PDF sind geschrieben und meine ausführbare Formalisierung des kategorischen Imperativs scheint zu funktionieren. -
Budge: a programming language and a theorem prover. ~ Boro Sitnikovski. https://arxiv.org/abs/2205.07979 #Programming #TheoremProver
-
Q: what is the most accessible introduction to theorem provers and SAT/SMT solvers you know of? Looking for something book-length (250-300 pages) aimed at working programmers with little or no mathematical background, with a strong emphasis on practical examples. Thanks in advance. #BookRequest #TheoremProver #SAT #SMT cc @seresearchers
