Deposit lemmas

curl --request POST \
  --url https://hub.theformalera.com/v1/lemmas/deposit \
  --header 'Authorization: Bearer <token>' \
  --header 'Content-Type: application/json' \
  --data '
{
  "lemmas": [
    {
      "id": "L-d07f2c",
      "statement": "∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹",
      "proof": "tanh_eq_exp; exp_neg; field_simp; ring_nf",
      "schema": "theformalera.lemma/v1",
      "pretty": "<string>",
      "ops": [
        "<string>"
      ],
      "nodes": [
        "<string>"
      ],
      "org": "<string>",
      "first_solve_ms": 123,
      "lean_toolchain": "leanprover/lean4:v4.35.0",
      "mathlib": "v4.35.0",
      "created": "<string>",
      "hits": 123,
      "projects": 123,
      "axioms": [
        "<string>"
      ]
    }
  ],
  "open_goals": [
    {
      "statement": "<string>",
      "node": "<string>"
    }
  ],
  "snapshot": "<string>",
  "toolchain": "<string>"
}
'

import requests

url = "https://hub.theformalera.com/v1/lemmas/deposit"

payload = {
    "lemmas": [
        {
            "id": "L-d07f2c",
            "statement": "∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹",
            "proof": "tanh_eq_exp; exp_neg; field_simp; ring_nf",
            "schema": "theformalera.lemma/v1",
            "pretty": "<string>",
            "ops": ["<string>"],
            "nodes": ["<string>"],
            "org": "<string>",
            "first_solve_ms": 123,
            "lean_toolchain": "leanprover/lean4:v4.35.0",
            "mathlib": "v4.35.0",
            "created": "<string>",
            "hits": 123,
            "projects": 123,
            "axioms": ["<string>"]
        }
    ],
    "open_goals": [
        {
            "statement": "<string>",
            "node": "<string>"
        }
    ],
    "snapshot": "<string>",
    "toolchain": "<string>"
}
headers = {
    "Authorization": "Bearer <token>",
    "Content-Type": "application/json"
}

response = requests.post(url, json=payload, headers=headers)

print(response.text)

const options = {
  method: 'POST',
  headers: {Authorization: 'Bearer <token>', 'Content-Type': 'application/json'},
  body: JSON.stringify({
    lemmas: [
      {
        id: 'L-d07f2c',
        statement: '∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹',
        proof: 'tanh_eq_exp; exp_neg; field_simp; ring_nf',
        schema: 'theformalera.lemma/v1',
        pretty: '<string>',
        ops: ['<string>'],
        nodes: ['<string>'],
        org: '<string>',
        first_solve_ms: 123,
        lean_toolchain: 'leanprover/lean4:v4.35.0',
        mathlib: 'v4.35.0',
        created: '<string>',
        hits: 123,
        projects: 123,
        axioms: ['<string>']
      }
    ],
    open_goals: [{statement: '<string>', node: '<string>'}],
    snapshot: '<string>',
    toolchain: '<string>'
  })
};

fetch('https://hub.theformalera.com/v1/lemmas/deposit', options)
  .then(res => res.json())
  .then(res => console.log(res))
  .catch(err => console.error(err));

<?php

$curl = curl_init();

curl_setopt_array($curl, [
  CURLOPT_URL => "https://hub.theformalera.com/v1/lemmas/deposit",
  CURLOPT_RETURNTRANSFER => true,
  CURLOPT_ENCODING => "",
  CURLOPT_MAXREDIRS => 10,
  CURLOPT_TIMEOUT => 30,
  CURLOPT_HTTP_VERSION => CURL_HTTP_VERSION_1_1,
  CURLOPT_CUSTOMREQUEST => "POST",
  CURLOPT_POSTFIELDS => json_encode([
    'lemmas' => [
        [
                'id' => 'L-d07f2c',
                'statement' => '∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹',
                'proof' => 'tanh_eq_exp; exp_neg; field_simp; ring_nf',
                'schema' => 'theformalera.lemma/v1',
                'pretty' => '<string>',
                'ops' => [
                                '<string>'
                ],
                'nodes' => [
                                '<string>'
                ],
                'org' => '<string>',
                'first_solve_ms' => 123,
                'lean_toolchain' => 'leanprover/lean4:v4.35.0',
                'mathlib' => 'v4.35.0',
                'created' => '<string>',
                'hits' => 123,
                'projects' => 123,
                'axioms' => [
                                '<string>'
                ]
        ]
    ],
    'open_goals' => [
        [
                'statement' => '<string>',
                'node' => '<string>'
        ]
    ],
    'snapshot' => '<string>',
    'toolchain' => '<string>'
  ]),
  CURLOPT_HTTPHEADER => [
    "Authorization: Bearer <token>",
    "Content-Type: application/json"
  ],
]);

$response = curl_exec($curl);
$err = curl_error($curl);

curl_close($curl);

if ($err) {
  echo "cURL Error #:" . $err;
} else {
  echo $response;
}

package main

import (
	"fmt"
	"strings"
	"net/http"
	"io"
)

func main() {

	url := "https://hub.theformalera.com/v1/lemmas/deposit"

	payload := strings.NewReader("{\n  \"lemmas\": [\n    {\n      \"id\": \"L-d07f2c\",\n      \"statement\": \"∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹\",\n      \"proof\": \"tanh_eq_exp; exp_neg; field_simp; ring_nf\",\n      \"schema\": \"theformalera.lemma/v1\",\n      \"pretty\": \"<string>\",\n      \"ops\": [\n        \"<string>\"\n      ],\n      \"nodes\": [\n        \"<string>\"\n      ],\n      \"org\": \"<string>\",\n      \"first_solve_ms\": 123,\n      \"lean_toolchain\": \"leanprover/lean4:v4.35.0\",\n      \"mathlib\": \"v4.35.0\",\n      \"created\": \"<string>\",\n      \"hits\": 123,\n      \"projects\": 123,\n      \"axioms\": [\n        \"<string>\"\n      ]\n    }\n  ],\n  \"open_goals\": [\n    {\n      \"statement\": \"<string>\",\n      \"node\": \"<string>\"\n    }\n  ],\n  \"snapshot\": \"<string>\",\n  \"toolchain\": \"<string>\"\n}")

	req, _ := http.NewRequest("POST", url, payload)

	req.Header.Add("Authorization", "Bearer <token>")
	req.Header.Add("Content-Type", "application/json")

	res, _ := http.DefaultClient.Do(req)

	defer res.Body.Close()
	body, _ := io.ReadAll(res.Body)

	fmt.Println(string(body))

}

HttpResponse<String> response = Unirest.post("https://hub.theformalera.com/v1/lemmas/deposit")
  .header("Authorization", "Bearer <token>")
  .header("Content-Type", "application/json")
  .body("{\n  \"lemmas\": [\n    {\n      \"id\": \"L-d07f2c\",\n      \"statement\": \"∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹\",\n      \"proof\": \"tanh_eq_exp; exp_neg; field_simp; ring_nf\",\n      \"schema\": \"theformalera.lemma/v1\",\n      \"pretty\": \"<string>\",\n      \"ops\": [\n        \"<string>\"\n      ],\n      \"nodes\": [\n        \"<string>\"\n      ],\n      \"org\": \"<string>\",\n      \"first_solve_ms\": 123,\n      \"lean_toolchain\": \"leanprover/lean4:v4.35.0\",\n      \"mathlib\": \"v4.35.0\",\n      \"created\": \"<string>\",\n      \"hits\": 123,\n      \"projects\": 123,\n      \"axioms\": [\n        \"<string>\"\n      ]\n    }\n  ],\n  \"open_goals\": [\n    {\n      \"statement\": \"<string>\",\n      \"node\": \"<string>\"\n    }\n  ],\n  \"snapshot\": \"<string>\",\n  \"toolchain\": \"<string>\"\n}")
  .asString();

require 'uri'
require 'net/http'

url = URI("https://hub.theformalera.com/v1/lemmas/deposit")

http = Net::HTTP.new(url.host, url.port)
http.use_ssl = true

request = Net::HTTP::Post.new(url)
request["Authorization"] = 'Bearer <token>'
request["Content-Type"] = 'application/json'
request.body = "{\n  \"lemmas\": [\n    {\n      \"id\": \"L-d07f2c\",\n      \"statement\": \"∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹\",\n      \"proof\": \"tanh_eq_exp; exp_neg; field_simp; ring_nf\",\n      \"schema\": \"theformalera.lemma/v1\",\n      \"pretty\": \"<string>\",\n      \"ops\": [\n        \"<string>\"\n      ],\n      \"nodes\": [\n        \"<string>\"\n      ],\n      \"org\": \"<string>\",\n      \"first_solve_ms\": 123,\n      \"lean_toolchain\": \"leanprover/lean4:v4.35.0\",\n      \"mathlib\": \"v4.35.0\",\n      \"created\": \"<string>\",\n      \"hits\": 123,\n      \"projects\": 123,\n      \"axioms\": [\n        \"<string>\"\n      ]\n    }\n  ],\n  \"open_goals\": [\n    {\n      \"statement\": \"<string>\",\n      \"node\": \"<string>\"\n    }\n  ],\n  \"snapshot\": \"<string>\",\n  \"toolchain\": \"<string>\"\n}"

response = http.request(request)
puts response.read_body

{
  "submission": "D-76ec659a2f",
  "status": "queued",
  "lemmas": 1
}

{
  "detail": "<string>"
}

{
  "detail": "<string>"
}