Lean 4: How the theorem prover works and why it's the new competitive edge in AI

https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in

#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).

#lean #theoremprover

100 theorems in Lean

https://leanprover-community.github.io/100.html

#HackerNews #100theorems #Lean #TheoremProver #Mathematics #Proofs

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.

#logic

Lol, ChatGPT предлагает мне, чтобы практиковаться в Agda следующее

> Решать задачи: Как и при изучении любого другого языка, практика очень важна. Вы можете решать задачи на sites, таких как Codewars или HackerRank, а также использовать ресурсы, такие как "The Agda Wiki", который предлагает ряд задач для решения.

Я сначала посмеялся, лет 5 назад я заходил на этот прекрасный сайт, кажется агдой там и не пахло, а сейчас захожу и там есть специальные задачи для Agda. Я в шоке. Сук, всё. Challenge accepted.

#Agda #ТеорияТипов #TypeTheory #TheoremProver

Mathematics can be reduced to a few logical principles. In other words, Mathematics is a closed world problem.

This may mean that, like Chess or Go, a machine is better doing math
than human. Automatic theorem proving was extensibly studied and resulted, for example, fast SAT solvers but to achieve human-like creativity, deep learning based approaches might be a way to go.

There are three approaches I can think of
- GPT like model (fashionable)
- Reinforcement learning (there are some)
- Diffusion model (?)

Diffusion model would be interesting because a mathematician starts with an intuitive but wrong idea then polishes it to a rigorous proof.

I'm also interested in "bootstrapping", i.e. starting without any training data.

Any idea or reference?

#DeepLearning #AutomatedTheoremProving #TheoremProver

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.

👉 https://github.com/diekmann/kant

#philosophy #math #Mathematik