From Newsgroup: comp.theory

Hi,

Lean nonsense is just Microsoft advertising.

Stefan Ram wrote:

Today we have Lean.

There were things like MIZAR, etc. before.

https://de.wikipedia.org/wiki/Mizar-System

But Lean has probably caught up with
MIZAR by now, regarding the amount of formalized
theories and proofs? Furthermore, the

combination with connectionist AI is probably
something newer and a result of the preceding Deep
Learning Revolution, whereas the current

AI boom stands out through improved natural
language processing and offers interesting
approaches to Chain of Thought and Agent Swarms.

But when I install Lean 4, the first thing you
notice is that it is a clunky system that is hard
to use and insistently screams to bring in a

Copilot, possibly with a paid subscription.

Bye

P.S: Or as Gemini puts it:

Lean Copilot is a plugin / an extension for the
Lean 4 compiler. It acts as a link between
your proof assistant and artificial intelligence.

Language Server (Lean 4 LSP): Lean Copilot hooks into
the Lean Language Server so that the AI suggestions
are displayed directly in your editor (e.g. VS Code)
while you type.

Local execution: You can run integrated open-source
models (like ReProver from LeanDojo) directly locally on
your own hardware (optional with GPU) without incurring
license or cloud fees
https://arxiv.org/html/2404.12534v3

It also supports connecting your own or external
LLMs, where depending on the external API provider used
(if you are not running a local server) costs for
model access may arise. Microsoft Copilot /
GitHub Copilot are the well-known, mostly paid
AI products from Microsoft.

Mild Shock schrieb:

Hi,

This is also cool, digging into some subtle
difference between the Natural Language text,
and the Lean Proof:

ABSTRACT. Autoformalisation is increasingly used to v
erify mathematical texts, including those generated by AI,
as in OpenAI’s announced proof of blow-up of solutions
to the Navier-Stokes equations. In this process, an AI
system translates the text from a natural language (NL)
into a formal language such as Lean.
https://arxiv.org/pdf/2610.08144

Bye

P.S.: I guess its time to download this plug-in
and do some Lean proofs by myself.

A Lean4 plugin for Jetbrains IDES https://plugins.jetbrains.com/plugin/25104-lean4ij

Disclaimer: Not affiliated with Jetbrains, there
is also a Lean 4 VS Code Extension.

LoL

--- Synchronet 3.22a-Linux NewsLink 1.2