BranchesTags

Repository files navigation

Code with Proofs: The Arena

Demo Site

Main essay: A Proposal for Safe and Hallucination-free Coding AI

This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.

The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.

The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges and create/manage submissions. Automatic API documentation available; once the app is running they are served at /docs (Swagger UI), and at /redoc (Redoc).

scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file in the format of Code with Proofs Benchmark.

Installation

Prerequisites

  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Installation Instructions

  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify

  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu: sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try psql with the current user, as suggested by this StackOverflow.

  2. In PostgreSQL prompt (replace with your password):

CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files: First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).

  2. poetry run alembic upgrade head

  3. ./run.sh

About

Lean coding problem solving challenge website with proof verification

Topics

lean4programmingproof

Resources

Readme
GPL-3.0 license
Activity

Stars

13 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

Packages

Used by

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
BranchesTags
Repository files navigation
Code with Proofs: The Arena
Demo Site
Main essay: A Proposal for Safe and Hallucination-free Coding AI
This repo implements a website with functionalities similar to online coding challenge sites like LeetCode, HackerRank and CodeForces, where users can submit solutions to coding challenges and be judged on test cases; except here the problems have function signatures with formal theorem statements, users submit code with proofs, and will be judged by the proof checker. Right now the only supported language is Lean, but I hope someone can extend it to other similar languages such as Coq, Idris, Dafny.
The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source models.
The web app is implemented in Python with the FastAPI library. Both web interface and API endpoints are available to create/manage challenges
and create/manage submissions. Automatic API documentation available; once the app is running
they are served at /docs (Swagger UI), and at /redoc (Redoc).
scripts/import_challenges.py is a simple script that creates challenges by importing from a JSONL file
in the format of Code with Proofs Benchmark.
Installation
Prerequisites
  1. Python 3.10 or higher
  2. PostgreSQL. E.g. on Ubuntu/Debian:
sudo apt-get update
sudo apt-get install postgresql postgresql-contrib
sudo systemctl start postgresql
sudo systemctl enable postgresql
  1. Poetry (Python package manager).
curl -sSL https://install.python-poetry.org | python3 -
  1. Lean 4.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Installation Instructions
  1. clone the repository. cd into the directory. Then poetry install to install dependencies
  2. Install dependencies, including Mathlib4 and SafeVerify.
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake update
lake build safe_verify
  1. Create a database and user in PostgreSQL. First, log into the server using psql as the superuser of the PosgresSQL installation. For Ubuntu:
sudo -u postgres psql. For Mac homebrew installation the user postgres is not installed; you might try
psql with the current user, as suggested by this StackOverflow.
  2. In PostgreSQL prompt (replace with your password):
CREATE DATABASE coding_challenge_db;
CREATE USER coding_challenge_user WITH PASSWORD 'your_password_here';
GRANT CONNECT ON DATABASE coding_challenge_db TO coding_challenge_user;
\c coding_challenge_db
GRANT USAGE, CREATE ON SCHEMA public TO coding_challenge_user;
GRANT ALL PRIVILEGES ON ALL TABLES IN SCHEMA public TO coding_challenge_user;
ALTER DEFAULT PRIVILEGES IN SCHEMA public GRANT ALL ON TABLES TO coding_challenge_user;
\q

  1. Then put the password you chose in the previous step (for connection to PostgreSQL) in the following config files:
First modify dotenv.example and save it as .env, and also in alembic.ini (around line 64).
  2. poetry run alembic upgrade head
  3. ./run.sh
About
Lean coding problem solving challenge website with proof verification
Topics
lean4programmingproof
Resources
Readme
GPL-3.0 license
Activity
Stars
13 stars
Watchers
1 watching
Forks
0 forks
Report repository
Releases
Packages
Used by
Contributors
Languages