mirek/Vibe-ITP
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Interactive theorem prover. Human-written kernel & axioms, AI-written proof language & proofs (with some human help). Based on 2nd-order logic & set-theory.
44 commits 1 branch 0 tags 5 MiB
  • C++ 91.5%
  • C 7.9%
  • Emacs Lisp 0.4%
  • Makefile 0.2%
Find a file
Exact
Mirek Olšák bac29f3fef meta theory mostly done
2026-06-04 23:02:44 +02:00
AGENTS.md merge temporary challenges into the proof files 2026-05-27 22:52:44 +02:00
arithmetics-challenges.lg binary data format checker (but no export yet) 2026-05-18 16:07:33 +02:00
arithmetics-features-showcase.pf first JIT prototype 2026-05-21 14:36:55 +02:00
arithmetics.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
aux-def-test.pf move challenges to parser 2026-05-18 11:42:22 +02:00
basic-challenges.lg further development, binary checker format, reasoning about tuples 2026-05-20 14:17:28 +02:00
basic.pf meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
binary_export.cpp starting with meta-reasoning 2026-05-30 23:16:17 +02:00
binary_export.h starting with meta-reasoning 2026-05-30 23:16:17 +02:00
binary_spec.md starting with meta-reasoning 2026-05-30 23:16:17 +02:00
binder-rewrite-test.pf arithmetics proofs 2026-05-16 17:42:06 +02:00
bytecode.cpp starting with meta-reasoning 2026-05-30 23:16:17 +02:00
check.c starting with meta-reasoning 2026-05-30 23:16:17 +02:00
check.h starting with meta-reasoning 2026-05-30 23:16:17 +02:00
check_test.c starting with meta-reasoning 2026-05-30 23:16:17 +02:00
code-reasoning.pf meta lifting theorems done 2026-06-01 01:07:31 +02:00
emulator.cpp meta theory mostly done 2026-06-04 23:02:44 +02:00
equality.cpp meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
facts.cpp first JIT prototype 2026-05-21 14:36:55 +02:00
inception_jit.c further development, binary checker format, reasoning about tuples 2026-05-20 14:17:28 +02:00
jit-challenge.lg proving and running the most basic program 2026-05-22 11:19:17 +02:00
jit_demo.c Arithmetics x86_64 specification 2026-05-24 03:19:01 +02:00
jit_demo.pf starting with meta-reasoning 2026-05-30 23:16:17 +02:00
lg-mode.el progress on code verification 2026-05-27 04:00:41 +02:00
lit-challenges.lg binary data format checker (but no export yet) 2026-05-18 16:07:33 +02:00
lit.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
logic.c meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
logic.h starting with meta-reasoning 2026-05-30 23:16:17 +02:00
logic.lg meta theory mostly done 2026-06-04 23:02:44 +02:00
Makefile meta reasoning progress 2026-05-31 13:57:51 +02:00
meta-binder-test.lg meta theory mostly done 2026-06-04 23:02:44 +02:00
meta-binder-test.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
meta-lifting.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
meta-lit.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
meta-rules.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
meta.cpp meta theory mostly done 2026-06-04 23:02:44 +02:00
meta.lg meta theory mostly done 2026-06-04 23:02:44 +02:00
meta.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
natbits-challenges.lg Arithmetics x86_64 specification 2026-05-24 03:19:01 +02:00
natbits.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
parser.cpp meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
prime-challenge.lg progress on code verification 2026-05-27 04:00:41 +02:00
prime-loop-code.pf starting with meta-reasoning 2026-05-30 23:16:17 +02:00
prime-loop.pf finish proof of prime check correctness 2026-05-27 22:40:09 +02:00
prime-main.pf starting with meta-reasoning 2026-05-30 23:16:17 +02:00
prime.pf starting with meta-reasoning 2026-05-30 23:16:17 +02:00
proposals.md meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
prover-features-test.pf meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
prover.cpp meta theory mostly done 2026-06-04 23:02:44 +02:00
prover.md meta lifting theorems done 2026-06-01 01:07:31 +02:00
README.md meta theory mostly done 2026-06-04 23:02:44 +02:00
records.cpp meta rules (modus ponens & instantiation), multiple binder support in meta 2026-06-02 14:34:01 +02:00
records.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
set-theory-challenges.lg more instructions, starting hangling flags 2026-05-23 09:42:35 +02:00
set-theory.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
spec-x86_64.lg meta theory mostly done 2026-06-04 23:02:44 +02:00
todo starting with meta-reasoning 2026-05-30 23:16:17 +02:00
tuple-challenges.lg further development, binary checker format, reasoning about tuples 2026-05-20 14:17:28 +02:00
tuple.cpp meta reasoning progress 2026-05-31 13:57:51 +02:00
tuple.pf meta theory mostly done 2026-06-04 23:02:44 +02:00
univ-challenges.lg meta theory mostly done 2026-06-04 23:02:44 +02:00
univ.pf meta theory mostly done 2026-06-04 23:02:44 +02:00

README.md

Vibe ITP

Try out:

make
# in any order
./parser logic.lg
./prover logic.lg set-theory-challenges.lg arithmetics-challenges.lg lit-challenges.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf
# Code verification stack
./prover logic.lg spec-x86_64.lg prime-challenge.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf natbits.pf tuple.pf univ.pf records.pf code-reasoning.pf prime.pf prime-loop.pf prime-loop-code.pf prime-main.pf
# Meta-theory stack
./prover logic.lg meta.lg meta-binder-test.lg --proofs basic.pf set-theory.pf arithmetics.pf lit.pf natbits.pf tuple.pf univ.pf records.pf meta.pf meta-lifting.pf meta-rules.pf meta-binder-test.pf meta-lit.pf

File structure

  • logic.lg: definitions & axioms (human written)
  • logic.c: the logical kernel (human written)
  • *.pf: proof files
  • *-challenges.lg: target problems
  • *.cpp: the parsing & proving features
  • emulator.cpp, *jit*: experiments with binary code, not related to the rest