Kako vemo, kaj vemo

class: center, middle
background-image: url(AlumniTeden_4_3_SI.png)
background-size: cover

# Kako vemo, kaj vemo?

Katja Berčič, UL FMF

`katjabercic.github.io/kako-vemo`

<!-- 
  Ne epistemologija 
  Kaj naredimo, če nečesa ne vemo? Gremo na internet (v knjižnico, vprašamo nekoga, ki zna)
  Kdaj iskalniki ne delajo dobro? Kadar nimamo prave ključne besede (ali kak drug razlog, da ne moremo z besedami)
  Kaj pa imamo v matematiki? :D

ste že kdaj poskusili iskati formule ali številke?

Kako lahko v matematični literaturi najdemo informacije, če nimamo pravih ključnih besed.
  Bolj konkretno: kako lahko matematik preveri, če je npr. dokazal nov izrek, ali nekdo izven matematike ugotovi, 
  kaj o določeni stvari vedo matematiki.

IDEJE
  * kompleksne stvari (izreke, matematične strukture) indeksiramo posredno
  * upoštevanje strukture: sintaktično drevo formule, izraza v formalni matematiki

-->

---

.img.center.cx[
  ![Coxeter p1](coxeter1.jpg)
]

---

.img.center.cx[
  ![Coxeter p2](coxeter2.png)
]

---

## Formule (simbolični zapisi)

.img.center.hd[
 ![FMF hoodie](fmf-hoodie.jpg)
]

---

## Formule (simbolični zapisi)

.searchtb[
 |                                              | Google | Bing |
 | -------------------------------------------- | ------ | ---- |
 | $a^2 + b^2 = c^2$                            | [1](https://www.google.com/search?q=a%5E2+%2B+b%5E2+%3D+c%5E2), [2](https://www.google.com/search?q=%C4%8D%5E2+%2B+%C5%A1%5E2+%3D+%C5%BE%5E2) | [1](https://www.bing.com/search?q=a%5E2+%2B+b%5E2+%3D+c%5E2), [2](https://www.bing.com/search?q=č%5E2+%2B+š%5E2+%3D+ž%5E2) |
 | $f(x) = x^2 + x + 41$                        | [1](https://www.google.com/search?q=f%28x%29+%3D+x%5E2+%2B+x+%2B+41), [2](https://www.google.com/search?q=%F0%9F%90%87%5E2+%2B+%F0%9F%90%87%C2%A0%2B+41) | [1](https://www.bing.com/search?q=x%5E2+%2B+x+%2B+41), [2](https://www.bing.com/search?q=🐇%5E2+%2B+🐇%C2%A0%2B+41) |
 | $x\_{r+1} = x\_r - \frac{f(x\_r)}{f'(x\_r)}$ | [1](https://www.google.com/search?q=x_%7Br%2B1%7D+%3D+x_r+-+%5Cfrac%7Bf%28x_r%29%7D%7Bf%27%28x_r%29%7D) | [1](https://www.bing.com/search?q=x_%7Br%2B1%7D+%3D+x_r+-+%5Cfrac%7Bf%28x_r%29%7D%7Bf%27%28x_r%29%7D) |
]

<!-- 
 $\sin^2 \phi + \cos^2 \phi = 1$
 $2 \tan^2 \phi + 2 = 2 \sec^2 \phi$
 $3 + 3 \cot^2 \phi = 3 \csc^2 \phi$

-->

---

## Načrt predavanja 1.0

1. Postavimo nekaj zvitih vprašanj iskalniku<br>
  $č^2 + š^2 = ž^2$
2. Vidimo, da so odgovori slabi:<br>
  "Zakon o upravnih taksah (ZUT)"
3. Imamo odlično motivacijo 🎉

---

## Načrt predavanja 1.0

.img.center[
  ![ChatGPT](chatgpt.jpg)
]

<!-- v naslednji uri bomo za nekaj časa pozabili na velike jezikovne modele
- ker je drugi pogled bolj zanimiv z matematičnega vidika
- ker še ne vemo, če lahko ti modeli dobro delujejo brez orodij v ozadju

Nisem še pogledala novejše verzije, ki zna delati tudi s slikami, ampak v resnici to nima veze.
Delež vprašanj, na katera nam bodo UI orodja znala odgovoriti, se bo zdaj večal.
Lahko pa pogledamo, kako so videti zanimiva vprašanja.
-->

---

## ChatGPT in načrt predavanja 2.0

Veliki jezikovni modeli prepoznajo vzorce odnosov med simboli.

1. ChatGPT v resnici ne naslovi izvorne težave
--

2. Ne dela: manj znana dejstva
--

3. Sledimo načrtu 1.0, ideje so vredne ogleda

---

## Kako delujejo iskalniki?

* _Pajek_ obiskuje spletne strani. _Razpoznavalnik_ poišče ključne besede.
  Indeks:
.searchtb.small[
| osnovni simbol              | dokumenti                   |
| --------------------------- |:--------------------------- |
| matematika                  | dokument 1, dokument 7, ... |
| formula                     | dokument 7, dokument 8, ... |
| iskalnik                    | dokument 1, dokument 5, ... |
]
* Iskanje rezultatov v indeksu, ki ustrezajo povpraševanju (PageRank)

---

## Iskanje formul (1/3)

Inženir išče dobro zgornjo mejo za integral

$\int_a^b |V(t) I(t)| dt$

Pomagamo si lahko s Hölderjevo neenakostjo:

$\int_l^h |f(x)g(x)| dx \leq (\int_l^h |f(x)|^p)^\frac{1}{p} (\int_l^h g(x)^1)^\frac{1}{q}$

---

## Iskanje formul (2/3)

Iskalnik MathWebSearch za formule v matematičnih člankih: 
  
[<img src="https://zbmath.org/static/zbmath@2x.gif" height="30px" />](https://zbmath.org/formulae/)

* v ozadju algoritem unifikacije
.right[
$a^2 + b^2 = c^2$

![AST Pitagora](ast-pitagora.png)
]

---

## Iskanje formul: prihodnost

S podobnimi pristopi kot za formule lahko poskusimo iskati tudi diagrame.

![diagram](pcbi.1005683.e039.PNG)

.footnote[
doi.org/10.1371/journal.pcbi.1005683
]
---

## Več, kot samo formule

### Koliko različnih vzorcev lahko sestavimo? (1/2)

<table class="tg">
<tbody>
  <tr>
    <td class="tg1 bt"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bt"></td>
    <td class="tg1 bt"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bt"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bt"></td>
    <td class="tg1 bt"></td>
  </tr>
  <tr>
    <td class="tg1 bb"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bb"></td>
    <td class="tg1 bb"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bb"></td>
    <td class="tg2"></td>
    <td class="tg2 br"></td>
    <td class="tg1 bb"></td>
    <td class="tg1 bb"></td>
  </tr>
</tbody>
</table>

<!-- 
  ## Matematično znanje
  ### Kako ga najdemo in uporabimo

* (Ključne) besede: 
    - `Pitagorov izrek`
    - `Fermatov veliki izrek`
  * Številke: 
    - `2, 3, 5, 7, 11, 13, 17, 19, 23, 29`
    - `3, 5, 8, 13, 21`
    - `1, 2, 5, 14, 42, 132`
  * Enačbe: 
    - $f(x) = x^2 + x + 41$,
    - $\sin^2 \phi + \cos^2 \phi = 1$
    - $2 \tan^2 \phi + 2 = 2 \sec^2 \phi$
    - $3 + 3 \cot^2 \phi = 3 \csc^2 \phi$
    - $x_{r+1} = x_r - \frac{f(x_r)}{f'(x_r)}
  * Diagrami
 -->

---

### Koliko različnih vzorcev lahko sestavimo? (2/2)

Širina 4:

* navpično domino in vzorec širine 3
* dve vodoravni domini in vzorec širine 2

.searchtb[
| Širina  |  0  |  1  |  2  |  3  |  4  |  5  |
| --------| --- | --- | --- | --- | --- | --- |
| [Število](https://www.google.com/search?q=1%202%203%205%208) |  ?  |  1  |  2  |  3  |  5  |  8  |
]

---

### Koliko različnih vzorcev lahko sestavimo? (3/3)

Enciklopedija številskih zaporedij OEIS:

- [1, 2, 3, 5, 8](https://oeis.org/search?q=1%2C+2%2C+3%2C+5%2C+8&language=english&go=Search)
  - vaše najljubše zaporedje?

<!--   
```
$\displaystyle e^{i\pi }+1=0$

integral u dv = uv - integral v du

integral x dy = xy - integral y dx

a^2 + b^2 = c^2

integral |f(x)g(x)| dx

integral |f(x)g(x)| dx bound theorem

``` 
-->

---

## Več kot številke in formule

### Grafi (1/3)

.img.center.pt[
![graf št. 1](i1.jpg)
]

---

## Več kot številke in formule

### Grafi (2/3): isti graf, kot prej

.img.center.hd[
![graf št. 2](i2.jpg)
]

---

## Več kot številke in formule

### Grafi (3/3):

* Znani problem izomorfizma grafov
* [House of Graphs](https://houseofgraphs.org/draw_graph)
* Kako lahko še najdemo graf?

---

## Kaj pa izreki?

Izrekov drugače kot posredno ne znamo iskati.

### Pitagorov izrek (1/2)

.hl[
.center[
$a^2 + b^2 = c^2,$
]
_kjer sta $a$ in $b$ dolžini katet, $c$ pa dolžina hipotenuze._
]

---

## Kaj pa izreki?

### Pitagorov izrek (2/2)

```
theorem 
  euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two 
  {V : Type u_1}  {P : Type u_2}  [normed_add_comm_group V]  
  [inner_product_space ℝ V] [metric_space P]  [normed_add_torsor V P]  
  (p1 p2 p3 : P) :
has_dist.dist p1 p3 * has_dist.dist p1 p3 = 
  has_dist.dist p1 p2 * has_dist.dist p1 p2 + 
  has_dist.dist p3 p2 * has_dist.dist p3 p2 
  ↔ euclidean_geometry.angle p1 p2 p3 = real.pi / 2
```

.hl[
_Tools such as Lean will one day help us mathematicians search for theorems in the literature, and help us to prove theorems._<br>
(Kevin Buzzard)
]

<!-- ---

## Za konec

Nekateri problemi niso rešljivi v vsej splošnosti.

V praksi imajo ti problemi pogostejše enostavne primere,
ki pa se jih da rešiti, in še več, pogosto so ti enostavnejši primeri tudi dovolj. -->

---

Povezave:

* [The On-Line Encyclopedia of Integer Sequences](https://oeis.org)
* [Fingerprint Databases for Theorems](https://www.ams.org/notices/201308/rnoti-p1034.pdf)
* [House of graphs](https://houseofgraphs.org)
* [The dawn of formalized mathematics](https://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf)
* [The future of mathematics?](https://www.ma.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf)