← Feed

Posts

• View post

  RE: https://lipn.info/@mevenlennonbertrand/116997917683191056 Scary. Also makes a case for funding fundamental type theory research in the age of AI

• View post

  A model that can't find vulnerabilities can't fix them, let alone formally prove their absence (for specific classes of vulnerabilies). When we keep those models out of the hands of the public, the bad actors will still find a way, but the public will be defenseless. Open weight is the future, and the sooner the US government sees that, the sooner they regain this country's once-comfortable lead in the AI race. For now, China will bask in this dual soft-power and hard-power win.

• View post

  Our synthetic Euclidean Geometry proof assistant is now open for public contributions! We created this together as a class in my Build Your Own Proof Assistant course this semester. Please give it a spin and consider contributing! https://github.com/nicegeo/nicegeo Some features: - Dependent-type-theory-based proof kernel - Synthetic Euclidean geometry layer (axiomatization of System E) with elaboration exhaustively tested - Tactic-based interactive proofs - Holes, bidirectional type checking...

• View post

  I'm looking for students interested in a paid summer research position: https://opportunities.cs.illinois.edu/research/paid-summer-research-opportunity-in-ai-for-program

• View post

  God, the social questions around AI and math are way harder than the technical questions

• View post

  We chose a target domain for our Build Your Own Proof Assistant class today. We are going to build a very encouraging and friendly proof assistant for middle/high-school geometry proofs. Any resources or tips for targeting this domain?

• View post

  How do people decide whether to submit a formalized mathematics paper to AFM or JAR? I think the emphases of the venues are different, but in this case I think we could write a paper with either emphasis. Right now my algorithm is just "ask my Ph.D. students which kind of paper they would rather write"

• View post

  We named the standard library for our Euclidean Geometry proof assistant "Euclib" and I'm so proud of this

• View post

  How do standard proof assistants handle motive inference for induction and rewriting? Especially interested in those that can actually do some kind of actual unification to tractably solve for all possible motives P, a la this ongoing issue in our geometry proof assistant: https://github.com/nicegeo/nicegeo/issues/182

• View post

  I am so tired

• View post

  Hey. I was banned from types.pl for having interviewed at the NSA 13 years ago, when I was 20 years old. I'm grateful for a new home on mathstodon. While I strongly appreciate the good-natured support from many of you, I am very unhappy with anyone who is going after the types.pl moderators personally for this and not just respectfully discussing the situation, and I'm personally extremely sorry if my Tweet inspired any of those actions. If I see this at all I will be escalating...

• View post

  Nobody warned me that humans can be this cute

• View post

  Whom will I see at the expMath kickoff?

• View post

  Found a bug in our synthetic layer of axioms, then asked Gemini 3 Pro to see if it could find any bugs in our axioms just by comparing our `env.txt` file with the source PDF we are formalizing. It did, without being pushed towards the particular axiom, even though there are like 40 axioms in this system. That is promising. (No idea if the rest of what it says is meaningful, will investigate.) https://github.com/nicegeo/nicegeo/issues/125

• View post

  Should I feel complimented or annoyed that proof repair (which I introduced in my Ph.D. thesis work) has become so commonplace that people don't even bother citing my work anymore when they do proof repair work?

• View post

  My niece, who is 10 years old, is two years ahead in math (this does not surprise me, because I watched her put together puzzles stating at 6 months). I'm visiting her now. In their math class, apparently they meet to discuss famous mathematicians once in a while. "That's so cool, I just came from a big meeting with a bunch of mathematicians!" I asked her if she remembered any they had spoken about and she couldn't remember lol

• View post

  If people are wondering what class prep looks like on my end for Build Your Own Proof Assistant, it's mostly organizing GitHub issues based on progress for the last sprint, and then writing specific goals for teams for the upcoming sprint that align with those issues and have concrete outcomes. So, basically, software engineering management.

• View post

  A few thoughts from talking to some of my favorite mathematicians (both for their work and, like, as people and friends) at the expMath meeting: 1. There is a big culture clash between math and AI, and it is really urgent that AI folks respect the mathematical culture if they want fruitful collaborations with math folks. (I remember this time in PL very well, in 2021-2022) 2. Never occurred to me that an emerging use case for proof repair is porting definitions, theorems, and proofs between on...