Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Galactica


Junyan Xu (Nov 17 2022 at 03:22):

sorry but this is hilarious :lol:
image.png
from Twitter

Junyan Xu (Nov 17 2022 at 03:28):

Here are some experiments I did with elliptic curves yesterday:
galactica.org
image.png image.png image.png

Gabriel Ebner (Nov 17 2022 at 04:38):

Clickable twitter link without the space: https://nitter.net/janosch_ortmann/status/1592635890471690240

Galactica web site: https://galactica.org/

Gabriel Ebner (Nov 17 2022 at 04:41):

OMG, this is hilarious:

Superposition theorem proving in Lean
This is a simple implementation of superposition in Lean, based on the SSReflect library. It can be used to prove ground theorems, given a set of ground axioms.
It is also possible to prove theorems that are universally quantified, using a ground term generator. This is not fully implemented yet.
The basic idea is that the user gives a set of axioms, and a theorem to prove, and Lean tries to find a proof using superposition. The theorem should be given in the form of an equality, since it is easier to work with, and the axioms should be equalities.

Floris van Doorn (Nov 17 2022 at 09:38):

:rolling_on_the_floor_laughing:
image.png

Johan Commelin (Nov 17 2022 at 09:47):

https://galactica.org/?prompt=Fermat%27s+Last+Theorem+in+Lean

We formalize the statement of Fermat's Last Theorem in the Lean theorem prover.

For an odd prime p, we define the statement of Fermat's Last Theorem fermat_last_theorem p as follows:

variables (p : N)

def fermat_last_theorem p : Prop :=
 (a b c : N),
  p  (a ^ p + b ^ p - c ^ p) 
  p  a  p  b  p  c

The N type denotes the natural numbers (nat), and p ∣ n denotes that p divides n.

In this formalization, we only consider the case of p being an odd prime.

Johan Commelin (Nov 17 2022 at 09:50):

https://galactica.org/?prompt=Liquid+Tensor+Experiment

Liquid Tensor Experiment

Liquid Tensor Experiment (LTE) is a video game developed by American studio Liquid Entertainment and published by Ubisoft for the Xbox 360. It was released on July 10, 2007 in North America and July 14, 2007 in Europe. It was the first Xbox 360 game to use Kinect, which is used to track the player's movements and control the game.

Gameplay

The game features a story-based single-player mode with eight levels, each with three sections. Players use Kinect to control the protagonist, an alien named Rex, through a series of levels. Players must complete a series of objectives to advance through the level. In the first section, Rex must navigate the level using only his telekinesis. The second section involves Rex using his "tenso" abilities, which are similar to the abilities of a liquid tensor. The third section requires

Junyan Xu (Nov 19 2022 at 16:00):

Demo is now offline
https://twitter.com/paperswithcode/status/1593259033787600896
https://twitter.com/ylecun/status/1593293058174500865
but models still available https://github.com/paperswithcode/galai


Last updated: Dec 20 2023 at 11:08 UTC