• Stars
    star
    104
  • Rank 322,935 (Top 7 %)
  • Language
    Prolog
  • Created over 4 years ago
  • Updated almost 4 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

It's a poorly named metamath verifier

twitchcoq -- a backspace.ai project

Reimplementing a subset of Coq in Python.

Just kidding, Coq is too complex. We implemented metamath instead.

It (slowly) verifies set.mm as of 11/3/2019

Ideally, Coq and friends should be rewritten in metamath. It's really the future, just wish it looked better. But omg, this is the proper stack for formal math, "formalism" is alive and well and is the truth in philosophy.

metamath as execution

We should be able to "run" a metamath program, aka proof without the target. It's a stack machine. The interpreter is only verifying that the proof is a valid program trace for the machine.

metamath on search

Take set.mm, remove all $p definitions. Find them with search. Powered by AI(tm).

"metasmash" written in C++17. First with the intermediate nodes in the graph. Then make it sparser. Then remove it altogether.

How many of the 71 Metamath theorems can we rediscover without the scaffolding?

Hmm, https://github.com/dwhalen/holophrasm

random notes

First order logic:

Theorem test : exists x : nat, x + 2 = 4.
Theorem test2 : forall y : nat, (exists x : nat, x = y).

Second order logic (quantifing over first order logic statements):

forall y : (fun x : nat -> nat)

Higher order logic...so on and so forth

randomer notes

Imagine twitch, but VR. We'll rebuild the cybercafes, the revolutionary coffee shops, the old hacker spaces, the town square, the churches, all of the trappings of civilization. But we'll build them in machines. We'll build them in math. We'll build them in homomorphically encrypted lockers. We'll build them where copies are free, tax is ridiculous, removing your landlord is a fork, and the only axis on which to compete is quality. True freedom of association.

We need embodiment to be free from the tyranny of owned space. And we need formalization to be secure.

The attacker vs defender battle may have been lost IRL. But in the world of information, the defender seems to win.

thoughts

To build a machine that can program.

  • How much of programming exists without real world context?
  • Refactoring definitely is, optimizing for some notion of "readability".
  • Speed definitely is, optimizing for well, speed.

metamath is just the program trace of a proof. Any language can be built on top of it to generate the trace.

Instead of proving two programs the same, can we prove two program traces the same? Depends on how we define the same, in the metamath sense, it's only the output at the end, aka easy.

Hehe, a program is just the compression of all of its traces. QIRA is AI lah

compression aside

Lossy compression has no meaning, though there is something aside from lossless compression. There's task specific compression, dealt with this at comma. The trees on the side of the road have no effect on the driving problem, and that's why a straight up lossless compressor isn't the goal function.

I think "Value Prediction Networks" (https://arxiv.org/abs/1707.03497) gets this right, would be fun to implement that. Correct to say you are just compressing to predict the reward?

Then there's the universal goal function of compression progress (https://arxiv.org/abs/0812.4360) as a way of separating noise (which will never be compressed), from signal (which will have a gradient of compression).

More Repositories

1

qira

QEMU Interactive Runtime Analyser
C
3,806
star
2

fromthetransistor

From the Transistor to the Web Browser, a rough outline for a 12 week course
3,512
star
3

minikeyvalue

A distributed key value store in under 1000 lines. Used in production at comma.ai
Go
2,791
star
4

corona

Reverse engineering SARS-CoV-2
Python
2,450
star
5

ai-notebooks

Some ipython notebooks implementing AI algorithms
Jupyter Notebook
959
star
6

twitchslam

A toy implementation of monocular SLAM written while livestreaming
Python
941
star
7

configuration

Like some files bro
Haskell
379
star
8

tinyvoice

Letting computers listen to you and really care
Jupyter Notebook
361
star
9

twitchchess

like twitchslam, for chess
Python
349
star
10

lolrecaptcha

We try to break the recaptcha for the Merry Christmas for all!
Go
292
star
11

mergesorts

mergesort in many languages
Shell
254
star
12

twitchcore

It's a core. Made on Twitch.
Verilog
229
star
13

cuda_ioctl_sniffer

Sniff CUDA ioctls
C
147
star
14

eda-reversing

The Embedded Disassembler
C++
110
star
15

kvm-kext

An implementation of /dev/kvm for Mac OS X
C
108
star
16

twitchtactoe

Tic Tac Toe in React because it is Simple Skills Sunday
JavaScript
102
star
17

battlechess

A distributed decentralized chess tournament
Python
99
star
18

tinyxxx

tiny corporation website
HTML
96
star
19

hammer-website

HTML
71
star
20

edgetpuxray

Enabling tinygrad compatibility with the Google Edge TPU
C++
68
star
21

pie

Computing digits of pi for the people
JavaScript
68
star
22

eda-2

Even better than eda-reversing...I hope
C++
61
star
23

haskell-scheme

Writing Scheme in Haskell
Haskell
58
star
24

twitchctw

compression = AI
Python
53
star
25

coq-hardy

Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
Coq
52
star
26

freethedsp

For winners only. Are you a winner?
C
40
star
27

twitchcoins

Python
36
star
28

openhexagon

An attempt at an open source toolchain for the Hexagon DSP
Shell
35
star
29

crappycase

So many shitty coders: Adobe, Blizzard, Valve. This is a case insensitivity emulator.
C
29
star
30

body_loop

comma body does a loop around the office
Python
28
star
31

amdgpu-dkms

Unpacking AMD's dkms packages
C
25
star
32

jenkyiphonetools

iPhone Tools of the lowest quality
Python
25
star
33

lowqualityraytracer

ever wonder how to raytrace? me too. i love america
Python
25
star
34

commaled

comma.ai LED controller cause the car needs some lights bro. SWAG!
Assembly
25
star
35

trinity-osxnew

C
22
star
36

aes_serial

There is so much swag in the world, just some of it is hidden -- Gandalf
C
17
star
37

eda-3

eda-3 from many years ago
JavaScript
13
star
38

collfun

It's Christmas time, you know what it is
Python
11
star
39

nnweights

6
star
40

7900xtx

5
star
41

gpysieve

ghetto sieves in python that don't work
Python
4
star
42

angr-travis

Run travis-ci testing on release version of angr
Shell
4
star
43

tt06-fp4-mac

FP4 MAC Array
Tcl
3
star
44

tt-twitch

tenstorrent kernel from twitch
C++
2
star