Search lemmas

curl --request GET \
  --url https://hub.theformalera.com/v1/lemmas \
  --header 'Authorization: Bearer <token>'

import requests

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

headers = {"Authorization": "Bearer <token>"}

response = requests.get(url, headers=headers)

print(response.text)

const options = {method: 'GET', headers: {Authorization: 'Bearer <token>'}};

fetch('https://hub.theformalera.com/v1/lemmas', 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",
  CURLOPT_RETURNTRANSFER => true,
  CURLOPT_ENCODING => "",
  CURLOPT_MAXREDIRS => 10,
  CURLOPT_TIMEOUT => 30,
  CURLOPT_HTTP_VERSION => CURL_HTTP_VERSION_1_1,
  CURLOPT_CUSTOMREQUEST => "GET",
  CURLOPT_HTTPHEADER => [
    "Authorization: Bearer <token>"
  ],
]);

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

curl_close($curl);

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

package main

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

func main() {

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

	req, _ := http.NewRequest("GET", url, nil)

	req.Header.Add("Authorization", "Bearer <token>")

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

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

	fmt.Println(string(body))

}

HttpResponse<String> response = Unirest.get("https://hub.theformalera.com/v1/lemmas")
  .header("Authorization", "Bearer <token>")
  .asString();

require 'uri'
require 'net/http'

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

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

request = Net::HTTP::Get.new(url)
request["Authorization"] = 'Bearer <token>'

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

{
  "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",
      "scope": "general",
      "schema": "theformalera.lemma/v1",
      "pretty": "<string>",
      "ops": [
        "<string>"
      ],
      "nodes": [
        "<string>"
      ],
      "source": "builtin",
      "visibility": "public",
      "org": "<string>",
      "first_solve_ms": 123,
      "lean_toolchain": "leanprover/lean4:v4.35.0",
      "mathlib": "v4.35.0",
      "created": "<string>",
      "hits": 123,
      "projects": 123,
      "status": "active",
      "axioms": [
        "<string>"
      ]
    }
  ]
}

{
  "detail": [
    {
      "loc": [
        "<string>"
      ],
      "msg": "<string>",
      "type": "<string>",
      "input": "<unknown>",
      "ctx": {}
    }
  ]
}