Lean Copilot Files

LLMs as Copilots for Theorem Proving in Lean

This is an exact mirror of the Lean Copilot project, hosted at https://github.com/lean-dojo/LeanCopilot. SourceForge is not affiliated with Lean Copilot. For more information, see the SourceForge Open Source Mirror Directory.

The interactive file manager requires Javascript. Please enable it or use sftp or scp.
You may still browse the files here.

Name	Modified	Size	InfoDownloads / Week
Parent folder
arm64-linux.tar.gz	2025-09-15	104.3 MB	0
x86_64-linux.tar.gz	2025-09-15	109.5 MB	0
arm64-macOS.tar.gz	2025-09-15	4.0 MB	0
README.md	2025-09-15	414 Bytes	0
v4.23.0 source code.tar.gz	2025-09-15	174.6 kB	0
v4.23.0 source code.zip	2025-09-15	194.3 kB	0
Totals: 6 Items		218.1 MB	0

What's Changed

latest stable version by @Peiyang-Song in https://github.com/lean-dojo/LeanCopilot/pull/174
Latest stable version by @Peiyang-Song in https://github.com/lean-dojo/LeanCopilot/pull/179
Bump to latest stable version Lean 4.23.0 by @Peiyang-Song in https://github.com/lean-dojo/LeanCopilot/pull/182

Full Changelog: https://github.com/lean-dojo/LeanCopilot/compare/v4.22.0...v4.23.0

Source: README.md, updated 2025-09-15

Other Useful Business Software

Gen AI apps are built with MongoDB Atlas

The database for AI-powered applications.

MongoDB Atlas is the developer-friendly database used to build, scale, and run gen AI and LLM-powered apps—without needing a separate vector database. Atlas offers built-in vector search, global availability across 115+ regions, and flexible document modeling. Start building AI apps faster, all in one place.

Start Free

Auth0 for AI Agents now in GA

Ready to implement AI with confidence (without sacrificing security)?

Connect your AI agents to apps and data more securely, give users control over the actions AI agents can perform and the data they can access, and enable human confirmation for critical agent actions.

Start building today

Recommended Projects

DeepSeek Prover V2
Advancing Formal Mathematical Reasoning via Reinforcement Learning
OpenLLM
Operating LLMs in production
LMDeploy
LMDeploy is a toolkit for compressing, deploying, and serving LLMs
GPT4All
Run Local LLMs on Any Device. Open-source
DeepSeekMath-V2
Towards self-verifiable mathematical reasoning

Lean Copilot Files

LLMs as Copilots for Theorem Proving in Lean

Get an email when there's a new version of Lean Copilot

What's Changed