funexists.github.io/index.html at main · funexists/funexists.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
<!doctype html>
<html>

<head>
  <meta charset="utf-8">
  <title>Fun Exists</title>
  <link rel="shortcut icon" href="favicon.ico" />

  <!-- github style -->
  <meta name="viewport" content="width=device-width, initial-scale=1, minimal-ui">
  <meta name="color-scheme" content="light dark">
  <link rel="stylesheet" href="github-markdown.css">
  <link rel="stylesheet" href="github-markdown-extra.css">
</head>

<body>
  <article class="markdown-body">
    <h1 align="center">
      <a href="https://github.com/funexists">
        <img alt="Fun Exists Logo" title="Fun Exists" width="96" src="./logo_flat.png" />
      </a>
      Fun Exists
    </h1>
    <p style="color:grey;" align="center">
      Fun &exist; pronounced the same as "fun e" or "funny".
      <a href="https://github.com/funexists">
        <img alt="GitHub" title="funexists's GitHub Account" height="24" width="24" src="./github.svg" />
      </a>
      <a href="https://www.youtube.com/@funexists">
        <img alt="YouTube" title="funexists's YouTube Channel" height="24" width="24" src="./youtube.svg" />
      </a>
    </p>

    </p>
      We are a group interested in mathematical programming for fun.
      This includes, but is not limited to: puns, game development in Lean and talks on Proof Assistants and Dependently Typed Programming.
    </p>

    <h2>Projects</h2>
    <ul>
      <li><a href="https://github.com/funexists/raylean">RayLean</a>: Lean4 bindings for Raylib</li>
      <li><a href="https://github.com/funexists/jessicacantswim">Jessica Can't Swim</a>: a game built using Raylean</li>
      <li><a href="https://github.com/funexists/coq-lean-cheatsheet">Coq Lean Cheatsheet</a>: a Cheatsheet for people transitioning from Coq to Lean</li>
    </ul>

    <h2>Presentations</h2>
    <ul>
      <li><a href="https://funexists.github.io/2025-stellenbosch/">The Little Typer reading group (Stellenbosch 2025)</a></li>
      <li><a href="https://github.com/funexists/ccc-talk">Correct Code by Construction (London 2022)</a></li>
      <li><a href="https://github.com/funexists/advertising-coq">Advertising Coq (Stellenbosch 2020)</a></li>
    </ul>

    <h2>Contact</h2>
    <p>mail @ funexists.com</p>

  </article>
</body>

</html>