Concept

Proof by contradiction

Publications associées (100)

Non-planarity of Markoff graphs mod p

We prove the non-planarity of a family of 3-regular graphs constructed from the solutions to the Markoff equation x2 + y2 + z2 = xyz modulo prime numbers greater than 7. The proof uses Euler characteristic and an enumeration of the short cycles in these gr ...

Berlin2024

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

Simon Guilloud

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

Controlling crystal cleavage in focused ion beam shaped specimens for surface spectroscopy

Philip Johannes Walter Moll, Matthias Carsten Putzke, Andrew Scott Hunter

Our understanding of quantum materials is commonly based on precise determinations of their electronic spectrum by spectroscopic means, most notably angle-resolved photoemission spectroscopy (ARPES) and scanning tunneling microscopy. Both require atomicall ...

Melville2024

A Gapless Post-quantum Hash Proof System in the Hamming Metric

Serge Vaudenay, Bénédikt Minh Dang Tran

A hash proof system (HPS) is a form of implicit proof of membership to a language. Out of the very few existing post-quantum HPS, most are based on languages of ciphertexts of code-based or lattice-based cryptosystems and inherently suffer from a gap cause ...

2023

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

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

Duality and bicrystals on infinite binary matrices

Thomas Gerber

The set of finite binary matrices of a given size is known to carry a finite type AA bicrystal structure. We first review this classical construction, explain how it yields a short proof of the equality between Kostka polynomials and one-dimensional sums t ...

2023

Gradient flow dynamics of shallow ReLU networks for square loss and orthogonal inputs

Nicolas Henri Bernard Flammarion, Etienne Patrice Boursier, Loucas Pillaud-Vivien

The training of neural networks by gradient descent methods is a cornerstone of the deep learning revolution. Yet, despite some recent progress, a complete theory explaining its success is still missing. This article presents, for orthogonal input vectors, ...

2022

Convex Quantization Preserves Logconcavity

Pol del Aguila Pla

A logconcave likelihood is as important to proper statistical inference as a convex cost function is important to variational optimization. Quantization is often disregarded when writing likelihood models, ignoring the limitations of the physical detectors ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2022

An automated do-it-yourself system for dynamic stem cell and organoid culture in standard multi-well plates

Matthias Lütolf, Sebastian Maerkl, Hao-An Hsiung, Zoe Newell Swank, Stefano Davide Vianello, Julia Tischler

We present a low-cost, do-it-yourself system for complexmammalian cell culture under dynamically changing medium formulations by integrating conventional multi-well tissue culture plates with simple microfluidic control and system automation. We demonstrat ...

2022

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