Galactica

Stream: Machine Learning for Theorem Proving

[Junyan Xu]

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

@ylecun @MetaAI @paperswithcode yeah... not sure this is ready yet https://twitter.com/janosch_ortmann/status/1592635890471690240/photo/1

- Janosch Ortmann (@janosch_ortmann)

[Junyan Xu]

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

[Gabriel Ebner]

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

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

[Gabriel Ebner]

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]

:rolling_on_the_floor_laughing:
image.png

[Johan Commelin]

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]

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]

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

Thank you everyone for trying the Galactica model demo. We appreciate the feedback we have received so far from the community, and have paused the demo for now. Our models are available for researchers who want to learn more about the work and reproduce results in the paper.

- Papers with Code (@paperswithcode)

Galactica demo is off line for now. It's no longer possible to have some fun by casually misusing it. Happy? https://twitter.com/paperswithcode/status/1593259033787600896

- Yann LeCun (@ylecun)