Skip to content
View shalashaska117's full-sized avatar
9 followers · 15 following

Achievements

Achievement: Pull Sharkx3Achievement: Pair ExtraordinaireAchievement: YOLOAchievement: Quickdraw

Achievements

Achievement: Pull Sharkx3Achievement: Pair ExtraordinaireAchievement: YOLOAchievement: Quickdraw

Highlights

  • Pro

Block or report shalashaska117

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
shalashaska117/README.md

Hi, I'm Pietro 👋

Automated reasoning, formal verification, and AI for mathematics.

I'm a CS student at the University of Naples Federico II and an AI researcher at Project Numina, working on automating mathematics with Numina Fuse. I also worked on the Lean 4 formalization of the three-dimensional Kakeya conjecture.

Portfolio LinkedIn Email

Open to internship and research opportunities.

Numina Fuse Kakeya in dimension three

Open source

Merged public pull requests, with counts for Vampire, Kakeya-3d, LiquidHaskell, and Apalache Pietro's public GitHub statistics, generated with GitHub Stats Extended

Vampire

I contribute correctness fixes and refactors to the Vampire theorem prover, from Boolean expressions and proof reconstruction to explicit container hashing.

Other contributions:

Personal projects

Fang

Fang repository: a first-order theorem prover in Rust with Lean 4 proof checking

I'm building Fang, an experimental first-order theorem prover in Rust with independent Lean 4 proof checking and TSTP output. My current focus is improving proof search.

Other projects:

  • ATL Model Checker: strategic verification of multi-agent systems. Python
  • Logic Evaluator: propositional logic and Boolean minimization. Python
  • DietiEstates25: real estate platform with geospatial search. Spring Boot · React · PostGIS

Technologies I've used

Programming languages
C++ C Java TypeScript Scala Rust Python Haskell JavaScript Go SQL

Proof assistants and verification tools
Lean 4 Vampire TPTP TLA+ Apalache LiquidHaskell

Web frameworks and databases
Spring Boot React Vue Node.js Express PostgreSQL PostGIS Redis Prisma

Development, testing, and writing
Git Linux Docker GitHub Actions Playwright LaTeX

Cards: GitHub Stats Extended. How the cards update.

Pinned Loading

  1. LASD_Project_2025 LASD_Project_2025 Public

    LASD - 2024/2025

    C++ 3

  2. atl-model-checker atl-model-checker Public

    Educational ATL model checker for strategic reasoning over concurrent game structures.

    Python

  3. logic-evaluator logic-evaluator Public

    Propositional logic evaluator and Boolean minimizer with parser, AST, truth tables, Quine-McCluskey, Petrick’s Method, and Karnaugh maps.

    Python

  4. Fang Fang Public

    Experimental first-order theorem prover in Rust, with Lean 4 proof checking and TSTP output.

    Lean 3

  5. vprover/vampire vprover/vampire Public

    The Vampire Theorem Prover

    C++ 449 85

  6. kakeya-3d kakeya-3d Public

    Forked from project-numina/kakeya-3d

    Lean