Skip to content

Instantly share code, notes, and snippets.

View 5HT's full-sized avatar
🌐
I'm very skeptical that person without empathy can create beautiful mathematics.

Namdak Tonpa 5HT

🌐
I'm very skeptical that person without empathy can create beautiful mathematics.
View GitHub Profile
Загальна картина: Чи може одна мова керувати всією математикою?
Уявіть, що вам доручено створити єдину мову програмування для кодування всього Всесвіту. Вона має обчислювати планетарні орбіти, писати прості програми, описувати квантову механіку та доводити кожну математичну теорему, коли-небудь задуману.
Десятиліттями математики та вчені-інформатики намагалися знайти цю «єдину універсальну мову».
Дехто вважав, що відповіддю є теорія множин. Інші вважали, що відповіддю є теорія гомотопічних типів (мова, заснована на геометрії).
У цій статті «Архітектура математики» робиться сміливе твердження: жодна окрема мова не може зробити все. Спроба створити монолітну мову — це як спроба створити швейцарський армійський ніж, який також є газонокосаркою, калькулятором і космічним кораблем. Він стає занадто важким і ламається під власною вагою.
Натомість у статті пропонується «Решітка мов» — мережа менших, вузькоспеціалізованих мов, які з'єднані автоматичними перекладачами (так званими «функторами»).
The Big Picture: Can One Language Rule All of Math?
Imagine you are tasked with building a single programming language to code the entire universe. It has to calculate planetary orbits, write simple apps, describe quantum mechanics, and prove every mathematical theorem ever conceived.
For decades, mathematicians and computer scientists have tried to find this "one universal language."
Some thought Set Theory was the answer.
Others thought Homotopy Type Theory (a language based on geometry) was the answer.
This paper, Architecture of Mathematics, makes a bold claim: No single language can do it all. Trying to build a monolithic language is like trying to build a Swiss Army knife that is also a lawnmower, a calculator, and a spaceship. It becomes too heavy and breaks under its own weight.
Instead, the paper proposes a Lattice of Languages—a network of smaller, highly specialized languages that are connected by automatic translators (called "functors").
This file has been truncated, but you can view the full file.
Checking: 2-quot₃
When trying to typecheck
λ (A : U), λ (R : Π (x₂₈₈₃₇₇ : A), Π (x₂₈₈₃₇₈ : A), U), λ (Q : Π (x : A), Π (y : A), Π (x₂₈₈₃₇₅ : R¯ A R x y), Π (x₂₈₈₃₇₆ : R¯ A R x y), U), λ (x : A), λ (y : A), λ (r1 : R¯ A R x y), λ (r2 : R¯ A R x y), λ (q : Q x y r1 r2), <i> <j> hcomp (2-quot A R Q) ((∂ i) ∨ (∂ j)) (λ (k : I), [(i = 0) → 2-quot₁ A R Q x, (i = 1) → (2-quot-path A R Q x y r2) @ (j ∨ k), (j = 0) → ι₂ (TotalSpokes A R Q) (PreHIT A R Q) (LHS_Stage2 A R Q) (RHS_Stage2 A R Q) (map_quot_pre A R Q (((trans-filler-p (quot A R) (quot₁ A R x) (quot₁ A R y) (quot₁ A R x) r1 (<i> r2 @ -i)) @ k) @ i)), (j = 1) → (2-quot-path A R Q x y r2) @ i]) ((resp (TotalSpokes A R Q) (PreHIT A R Q) (LHS_Stage2 A R Q) (RHS_Stage2 A R Q) ((x, (y, (r1, (r2, q)))), loop @ i)) @ j)
Against type
Π (A : U), Π (R : Π (x₂₈₈₃₅₉ : A), Π (x₂₈₈₃₆₀ : A), U), Π (Q : Π (x : A), Π (y : A), Π (x₂₈₈₃₅₇ : PathP (<x₉₅> coequ (Σ (x : A), Σ (y : A), R x y) A (λ (p : Σ (x : A), Σ (y : A), R x y), p.1) (λ (p : Σ (x : A), Σ (y : A), R x y), p.2
@5HT
5HT / client.txt
Created March 22, 2026 03:27
Zen Crypted Client Developer
Zen Crypted Backend Developer
=============================
Statement of Work – Client Developer (Swift / iOS / ASN.1)
*Project*: Development and enhancement of secure military-grade iOS chat client
*Position*: iOS Developer (Swift, security-focused)
*Project context*: The client is based on the open-source Chat X.509 for iOS, a server-less proof-of-concept using multicast UDP + X.509 certs for local encrypted messaging. The goal is to evolve it into a full client for the custom Elixir server (TCP/QUIC + ASN.1/DER protocol), with end-to-end X.509 CMS encryption and military-grade security.
Scope of Work (main deliverables):
@5HT
5HT / server.txt
Last active March 22, 2026 03:23
Zen Crypted Backend Developer
Zen Crypted Backend Developer
=============================
Statement of Work – Backend Developer (Elixir / Erlang / ASN.1)
*Project*: Development and enhancement of secure military-grade instant messaging server
*Position*: Senior/Middle Backend Developer (Elixir primary, Erlang/OTP understanding required)
*Project context*: The company is building a high-security chat platform for defense/government use cases.
The backend is based on the open-source CHAT server, which implements a custom ASN.1/DER-encoded protocol
over TCP/QUIC with full X.509 CMS envelope encryption, OCSP/LDAP validation, ephemeral messages,
@5HT
5HT / pis-il.txt
Created March 19, 2026 14:06
pis-il.txt
%{
name: "il",
protocol: "http",
connect_timeout: 60000,
read_timeout: 60000,
retries: 5,
url: "http://api-svc.pis-il/",
write_timeout: 60000,
plugins: ref(["plugins/prometheus"]),
routes: [
@5HT
5HT / package.txt
Created March 4, 2026 13:00
package.txt
Package: #{<<"containedItemQuantity">> => [],
<<"description">> =>
<<209,128,208,190,208,183,209,135,208,184,208,189,32,208,180,
208,187,209,143,32,209,150,208,189,96,209,148,208,186,209,134,
209,150,208,185,44,32,52,32,208,188,208,179,47,208,188,208,
187,59,32,208,191,208,190,32,49,32,208,188,208,187,32,208,176,
208,177,208,190,32,208,191,208,190,32,50,32,208,188,208,187,
32,208,178,32,208,176,208,188,208,191,209,131,208,187,208,176,
209,133,32,209,129,208,186,208,187,209,143,208,189,208,184,
209,133,32,208,183,32,208,177,209,128,209,131,208,189,208,176,
@5HT
5HT / gravity.txt
Created March 3, 2026 21:21
gravity.txt
Gravity Theories Dichotomy Tree
(Branching based on key decision points: conceptual, mathematical, and physical choices leading to each theory's existence)
Root: Fundamental View of Gravity
├── As a Field (Classical, Force-based)
│ ├── Non-Relativistic (Absolute time/space)
│ │ ├── Scalar Potential (Newtonian Gravity)
│ │ │ - Decision: Instantaneous action? Yes → Poisson's equation (∇²φ = 4πGρ)
│ │ │ - Exists due to: Empirical laws (e.g., inverse square) + field concept from EM analogy
│ │ └── Tensorial Reformulation (To geometrize)
@5HT
5HT / 2026-03-01 KVS.md
Created March 1, 2026 05:29
2026-03-01 KVS.md

Про доречність використання KVS

Про доречність використання KVS в Документообігах, CRM, чатах та телеком системах.

Вступ до KVS

KVS (Key-Value Store) — це легкий клієнтський інтерфейс, побудований на абстракціях баз даних типу B-tree, призначений для простого зберігання та обробки даних в Erlang/OTP-екосистемі. Розроблений компанією Synrc, KVS надає абстрактний, компактний та перевірений на практиці API (близько 500 рядків коду), який підтримує базові операції для систем, таких як леджери, месенджери, системи зберігання та банківські додатки.

# DevOps Engineer Vacancy
**Governmental Statistical Warehouse for National Healthcare Services**
**Position Title:** DevOps Engineer
**Department:** Information Technology and Data Management
**Location:** Kyiv, Ukraine (Hybrid / Remote options available)
**Employment Type:** Full-Time Contract
**Contract Duration:** Initial 12 months (with high probability of extension)
**Reporting To:** IT Project Manager
**Application Deadline:** March 15, 2026