Concept

Computer-assisted proof

Publications associées (44)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024

Computer-assisted proof of kernel inequalities

Maryna Viazovska, Abhinav Kumar

This data set provides a computer-assisted proof for the kernel inequalities needed to prove universal optimality in the paper "Universal optimality of the E_8 and Leech lattices and interpolation formulas" (by Cohn, Kumar, Miller, Radchenko, and Viazovska ...

EPFL Infoscience2023

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

2023

Beyond undulation! Body morphology and sensing components of elongated animals and robots reveal skills to maintain competent locomotion

Laura Isabel Paez Coy

Locomotion is an essential evolutive innovation of living beings that allows them to colonize and dominate the planet. As diverse as animal morphologies are (living) and were (extinct), their locomotion modalities are also diverse. In particular, animal mo ...

EPFL2023

Byzantine-Resilient Learning Beyond Gradients: Distributing Evolutionary Search

Rachid Guerraoui, Andrei Kucharavy, Matteo Monti

Modern machine learning (ML) models are capable of impressive performances. However, their prowess is not due only to the improvements in their architecture and training algorithms but also to a drastic increase in computational power used to train them.|S ...

New York2023

Effective Inhibition of TDP-43 Aggregation by Native State Stabilization

Hilal Lashuel, Yllza Jasiqi, Lixin Yang

Preventing the misfolding or aggregation of transactive response DNA binding protein with 43 kDa (TDP-43) is the most actively pursued disease-modifying strategy to treat amyotrophic lateral sclerosis and other neurodegenerative diseases. In this work, we ...

Weinheim2023

Slice-Less Optical Arbitrary Waveform Measurement (OAWM) in a Bandwidth of More Than 600 GHz

Tobias Kippenberg, Grigorii Likhachev

We demonstrate an optical arbitrary waveform measurement (OAWM) technique that exploits optical frequency combs as multi-wavelength local oscillators (LO) and that does not require any optical slicing filters. In a proof-of-concept experiment, we achieve r ...

IEEE2022

A proof of the instability of AdS for the Einstein-massless Vlasov system

Georgios Moschidis

In recent years, the conjecture on the instability of Anti-de Sitter spacetime, put forward by Dafermos-Holzegel (Dynamic instability of solitons in 4 + 1 dimesnional gravity with negative cosmological constant, 2006. https://www.dpmms.cam.ac.uk/similar to ...

SPRINGER HEIDELBERG2022

A Toolbox for Barriers on Interactive Oracle Proofs

Alessandro Chiesa

Interactive oracle proofs (IOPs) are a proof system model that combines features of interactive proofs (IPs) and probabilistically checkable proofs (PCPs). IOPs have prominent applications in complexity theory and cryptography, most notably to constructing ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Switchover phenomenon induced by epidemic seeding on geometric networks

Gergely Odor

It is a fundamental question in disease modeling how the initial seeding of an epidemic, spreading over a network, determines its final outcome. One important goal has been to find the seed configuration, which infects the most individuals. Although the id ...

2021

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search