Mina BH Arsanious ✶ homepage

about_me.txt

I am a third-year undergraduate student in Pure Mathematics at Cairo University, Giza. My interests span the foundations and philosophy of mathematics, combinatorics, formal proof assistants, and algebra. I am drawn to questions that sit at the boundary between mathematics and its own foundations, what mathematical objects are, how proofs can be mechanically verified, and what it means for a theorem to be true.

Outside of coursework I contribute to the Online Encyclopedia of Integer Sequences (OEIS), organize and speak at the Cairo University Mathematics Club, and run a Homotopy Type Theory reading group.

🎓

Institution
Cairo University, Giza

📘

Degree (Currently Doing)
B.Sc. Pure Mathematics (2024–present)

🔢

OEIS name
Mina BH Arsanious

research_log.txt

Pioneer Academics Research Scholarship Feb 2023 – Aug 2023

Supervised by Prof. Gregory Dresden, Washington & Lee University

Conducted individual research on Fibonacci numbers and visual combinatorial proofs, beginning with tiling problems (squares and dominoes) from Benjamin & Quinn's Proofs That Really Count. Developed original identities by translating carbon-bonding rules in complex hydrocarbons into combinatorial sequences, an approach that yielded new formulas and theorems proved jointly with my supervisor.

Derived a formula for the partial sums of sequence A006356, now featured on its OEIS page.
Contributed an entry on digit sequences avoiding certain patterns: A214997.

my_projects

Math Art Gallery 🚧 under construction

This is the main gallery that I try to update as I get some new stupid ideas to draw and explain how I drew them.

Built with Hugo · MathJax · TikZJax

lossmeme On GitHub!

A LaTeX package released under the LPPL license, with source and documentation maintained on GitHub.

LaTeX · LPPL

HoTT Reading Group Ongoing!

A Discord-based reading group working through Homotopy Type Theory, structured in phases starting with Altenkirch's Naive Type Theory before moving into the HoTT Book. Sessions are recorded and accompanied by session notes.

Discord · TikZ · Beamer

Kleene Realizability in Lean 4 🚧 work in progress

Formalizing Kleene realizability using Mathlib's pairing functions, building on an earlier formalization of the LEM to LPO implication.

Lean 4 · Mathlib

Cubical Agda Set up!

Set up a Cubical Agda environment as a hands-on companion to learning Homotopy Type Theory.

Agda · Cubical

seminar_archive.exe

I am an active member and co-supervisor of the Cairo University Mathematics Club, where I help lead recruitment and organize a seminar programme for new students.

01

Leaning into LEAN (2nd year, 2nd semester)

An introduction to the Lean 4 theorem prover and the Mathlib library, covering the Curry–Howard correspondence, and dependent types.
⬇ Download Presentation

02

Is Mathematics Real? (2nd year, 1st semester)

An expository talk on the ontological status of mathematical objects.
▶ Open Presentation

03

The Math of Molecules (1st year)

Presented the mathematics behind my Pioneer Academics research: combinatorial techniques, tiling identities, and chemically inspired integer sequences.

skills_config.sys

Mathematical Interests

Foundations of Mathematics & Mathematical Philosophy
Combinatorics & Integer Sequences
Formal Proof & Type Theory (Lean 4, Mathlib, Cubical Agda)
Abstract & Linear Algebra
Mathematical Visualization

Technical Skills

LaTeX & TikZ (including XeLaTeX workflows)
Lean 4 and Cubical Agda, formal proof writing
General programming (Linux, bash)
Desmos & mathematical visualization tools
Technical writing & mathematical exposition

Languages

Arabic (native, including Egyptian colloquial)
English (fluent)

guestbook.db

I am happy to discuss mathematics, research, or potential collaboration.

✍ SIGN MY GUESTBOOK

(entries are delivered by the ancient mailto protocol ✦ truly authentic. email: basiliousmina2@gmail.com)

about_me.txt_□✕

research_log.txt_□✕

my_projects_□✕

seminar_archive.exe_□✕

skills_config.sys_□✕